- Haskell - Haskell.org

ANNOUNCE: HSQL 1.0 released
by Krasimir Angelov 08 Sep '03

08 Sep '03

Dear Haskellers I am pleased to announce HSQL 1.0. The package is intended to give access to PostgresSQL, MySQL and ODBC databases. The HSQL is a part of HToolkit project but like GIO and Port it can be distributed as separate bundle. This is the first public release but as far as I know the package is already used in some other projects. I make this release with hope to makes HSQL more useful and more user friendly for other people working in Haskell. What is new? - The HSQL is separated from GUI part of the old HToolkit package. - Improved configure/make build system - the getSqlValue function from SqlBind type class is renamed to fromSqlValue. In SqlBind is defined new function - toSqlValue. The new function converts a Haskell value to its equivalent string representation in SQL syntax. - Improved support for geometric and network types for PostgreSQL. - Some bugfixes How to build? $ ./configure --enable-<backend> $ make $ make install where <backend> is one of: - mysql - postgres - odbc It is possible to build library with more than one backend. Just type: $ ./configure --enable-postgres --enable-odbc --enable-mysql Cheers Krasimir __________________________________ Do you Yahoo!? Yahoo! SiteBuilder - Free, easy-to-use web site design software http://sitebuilder.yahoo.com

1 0

CFP: CLIMA IV - Deadline Extended
by João Alexandre Leite 08 Sep '03

08 Sep '03

========================================================================== CALL FOR PAPERS CLIMA IV Fourth International Workshop on Computational Logic in Multi-Agent Systems January 6-7, 2004, Fort Lauderdale, Florida, USA http://centria.di.fct.unl.pt/~jleite/climaIV/index.htm Post-Proceedings will be published in Springer Verlag LNAI ***new*** Submission Deadline: September 26th Co-located with the 7th LPNMR and the 8th AIMATH =========================================================================== Over recent years, the notion of agency has claimed a major role in defining the trends of modern research. Influencing a broad spectrum of disciplines such as Sociology, Psychology, Philosophy and many more, the agent paradigm virtually invaded every sub-field of Computer Science, not least because of the Internet and Robotics. Multi-agent Systems (MAS) are communities of problem-solving entities that can perceive and act upon their environments to achieve their individual goals as well as joint goals. The work on such systems integrates many technologies and concepts in artificial intelligence and other areas of computing. There is a full spectrum of MAS applications that have been and are being developed; from search engines, educational aids to electronic commerce and trade. Although commonly implemented by means of imperative languages, mainly for reasons of efficiency, the agent concept has recently increased its influence in the research and development of computational logic based systems. Computational Logic, by virtue of its nature both in substance and method, provides a well-defined, general, and rigorous framework for systematically studying computation, be it syntax, semantics, procedures, or implementations, environments, tools, and standards. The purpose of this workshop is to discuss techniques, based on computational logic, for representing, programming and reasoning about multi-agent systems in a formal way. This is clearly a major challenge for computational logic, to deal with real world issues and applications. Following the workshop on Multi-Agent Systems in Logic Programming affiliated with ICLP'99, the first CLIMA workshop took place in London, UK, affiliated with CL'2000. The 2001 edition of CLIMA, took place in Paphos, Cyprus, affiliated with ICLP'01. CLIMA'02 took place in Copenhagen, Denmark, and was affiliated with ICLP'02 and part of FLOC'02. We solicit unpublished papers that address formal approaches to multi-agent systems. The approaches as well asbeing formal must make a significant contribution to the practice of multi-agent systems. Relevant techniques include, but are not limited to, the following: * Nonmonotonic reasoning in MAS * Planning under incomplete information in MAS * Logical foundations of MAS * Usage of abduction in MAS * Representation of knowledge and belief in MAS * Knowledge and belief updates in MAS * Temporal reasoning for MAS * Theory of argumentation for MAS * Negotiation and co-operation for MAS * Communication languages for MAS * Distributed constraint satisfaction in MAS * Modal logic approaches to MAS * Logic based programming languages for MAS * Distributed theorem proving for MAS * Logic based implementations of MAS * Decision theory for MAS * Logic based agents for the Internet SUBMISSION INSTRUCTIONS We welcome and encourage the submission of high quality, original papers, which are not simultaneously submitted for publication elsewhere. Please refer to the workshop web pages for further instructions concerning the submission procedures. IMPORTANT DATES * Submission: September 26th, 2003 * Notification of Acceptance: October 31th, 2003 * Final version due: November 28th, 2003 * CLIMA IV: January 6-7th, 2004 PROCEEDINGS Post-proceedings will be published by Springer-Verlag as a volume of the Lecture Notes on Artificial Intelligence (LNAI) series. Informal proceedings will be available at the workshop and online. PROGRAM COMMITTEE * Chitta Baral, Arizona State University, USA * Gerd Brewka, University of Leipzig, Germany * Jürgen Dix, The University of Manchester, UK * Thomas Eiter, Vienna University of Technology, Austria * Klaus Fischer, DFKI, Germany * Michael Fisher, University of Liverpool, UK * James Harland, Royal Melbourne Inst. of Tech., Australia * Katsumi Inoue, Kobe University, Japan * Gerhard Lakemeyer, Aachen Univ. of Technology, Germany * João Leite, New University of Lisbon, Portugal * Yves Lespérance, York University, Canada * John Jules Ch. Meyer, Univ. of Utrecht, The Netherlands * Leora Morgenstern, IBM, USA * Luís Moniz Pereira, New University of Lisbon, Portugal * Fariba Sadri, Imperial College, UK * Ken Satoh, National Institute of Informatics, Japan * Renate Schmidt, The University of Manchester, UK * Guillermo Simari, Universidad Nacional del Sur, Argentina * V. S. Subrahmanian, University of Maryland, USA * Francesca Toni, Imperial College, UK * Paolo Torroni, University of Bologna, Italy * Wiebe van der Hoek, University of Liverpool, UK * Cees Witteveen, Delft Univ. of Tech., The Netherlands WORKSHOP ORGANIZERS: * Jürgen Dix, The University of Manchester, UK (dix(a)cs.man.ac.uk) * João Leite, New University of Lisbon, Portugal (jleite(a)di.fct.unl.pt) INQUIRIES: Please send program suggestions and inquires to either of the organizers.

1 0

RE: Fundep & Datatype Request
by Simon Peyton-Jones 08 Sep '03

08 Sep '03

Another tricky one. There are at least two difficulties. 1. Consider the simpler function foo :: Fc Bool b => [b] -> Int foo (x:xs) = x Since b must be Int, you might argue that this function is OK, but GHC rejects it because it unifies the signature type variable b. This is a "legitimate" constraint on 'b'. The question is how to distinguish the legitimate constraints on b from the illegitimate ones. In principle, not too hard -- just "improve" the type signature, but GHC translates the whole thing to System F, so it really will pass a type parameter for 'b'... Maybe it can be done, but I feel queasy about it. 2. Suppose we have makeF3 i = [MkF2 i, ...., (undefined :: F2 Bool)] When type-checking MkF2 it's less obvious that the result will be an (F2 Bool) than it was in your example. So perhaps type-correctness depends on the "pushing-types-inwards" idea. Well, ok, that's what I do for higher-rank types, but we'd need to precisely say what programs are accepted and what programs are not. At the moment I'm somewhat resisting making further ad-hoc "improvements" to GHC's type-inference algorithm, even though it falls short in various ways, because I keep hoping someone is going to come up with a simple non-ad-hoc story that will address these various issues in a more systematic way. Simon | -----Original Message----- | From: haskell-admin(a)haskell.org [mailto:haskell-admin@haskell.org] On Behalf Of Ashley Yakeley | Sent: 05 September 2003 01:24 | To: haskell(a)haskell.org | Subject: Fundep & Datatype Request | | OK, this is an issue I have raised before I think, but I don't remember | what the opinion on it was. The following doesn't compile with ghc | -fglasgow-exts (or Hugs -98): | | -- ghc -fglasgow-exts -c TypeLambda.hs | module TypeLambda where | { | class Fc a b | a -> b; | | instance Fc Bool Int; | | data F1 a = forall b. (Fc a b) => MkF1 b; | | makeF1 :: Int -> F1 Bool; | makeF1 = MkF1; | | getF1 :: F1 Bool -> Int; | getF1 (MkF1 i) = i; | | data F2 a = MkF2 (forall b. (Fc a b) => b); | | makeF2 :: Int -> F2 Bool; | makeF2 i = MkF2 i; | | getF2 :: F2 Bool -> Int; | getF2 (MkF2 i) = i; | } | | Clearly makeF1 and getF2 are OK. But I claim getF1 and makeF2 should | compile, since the type inside either an "F1 Bool" or an "F2 Bool" must | always be an Int. Instead I get this: | | | TypeLambda.hs:14: | Inferred type is less polymorphic than expected | Quantified type variable `b' is unified with `Int' | When checking an existential match that binds | i :: b | and whose type is F1 Bool -> Int | In the definition of `getF1': getF1 (MkF1 i) = i | | TypeLambda.hs:19: | Cannot unify the type-signature variable `b' with the type `Int' | Expected type: b | Inferred type: Int | In the first argument of `MkF2', namely `i' | In the definition of `makeF2': makeF2 i = MkF2 i | | | So why is this useful? Because you can do some form of type-lambda with | it. For instance, you might have some system of collection types: | | Word8 -->> UArray Int Word8 | Word16 -->> UArray Int Word16 | (a -> b) -->> Array Int (a -> b) | | It would be nice to hide the implementation and just expose some | type-constructor: | | MyCollection Word8 | MyCollection Word16 | MyCollection (a -> b) | | I believe this can't be done currently. | | -- | Ashley Yakeley, Seattle WA | | _______________________________________________ | Haskell mailing list | Haskell(a)haskell.org | http://www.haskell.org/mailman/listinfo/haskell

1 0

RE: Haskell for non-Haskell's sake
by Simon Marlow 08 Sep '03

08 Sep '03

> I implemented a trivial "database", stored in ordinary files, > and had to > ensure mutual exclusion of database access between > simultaneously running > CGI scripts. Since each CGI run is short, I simply locked the entire > database for the entire run. Claiming a lock on a file is > easy in C (well, > it takes 18 lines...), but there's nothing in the standard Haskell > libraries that can do it. So I borrowed a little C code from > the net, and > called it via the FFI. Locking support is available in the unix package distributed with GHC. See: http://www.haskell.org/ghc/docs/latest/html/unix/System.Posix.IO.html#7 Cheers, Simon

2 1

SVV'03 call for papers
by Abhik Roychoudhury 08 Sep '03

08 Sep '03

(Apologies if you receive multiple copies of this message) SECOND CALL FOR PAPERS [ Submission deadline: September 15, 2003 ] *************************************************** International Workshop on Software Verification and Validation (SVV 2003) In Conjunction with International Conf. on Logic Programming (ICLP) 2003 Mumbai (India), December 2003 URL: http://www.comp.nus.edu.sg/~abhik/SVV03/index.html *********************************************** -------------------------------------- Topics Covered --------------------------------------- The workshop will focus on theoretical techniques, practical methods as well as case studies for verification of conventional and embedded software systems. In particular, we welcome papers which describe combinations of formal and informal reasoning, as well as formal verification and program analysis techniques. Tool papers and case studies, which report on advances in verifying large scale programs in standard languages are particularly sought. The list of topics include, but are not restricted to: Tools/environments/case studies for large scale software verification Static analysis/Abstract interpretation/Program transformations for verification Use of model checking and deductive techniques for software verification Role of declarative programming languages (such as Prolog) for infinite state verification. Techniques to validate system software (such as compilers) as well as assembly code/Java byte-code Proof techniques for verifying specific classes of software (such as object-oriented programs) Integrating testing and run-time monitoring with formal techniques Validation of UML diagrams, and/or requirement specifications Software certification and proof carrying code Integration of formal verification into software development projects ------------------------------- Workshop Format ----------------------------- The one day workshop will mostly involve talks of peer reviewed research papers in an informal setting. We plan to have several break-out sessions apart from the research paper sessions to promote informal discussions. In addition, there will be an invited talk (detailed information given below). ----------------------------- Submissions Information ------------------------------ Regular submissions should be no more than 15 pages. Short papers (up to 5 pages) describing initial ideas are also welcome. All submitted papers should be in PS or PDF. Please avoid using zip, gzip, compress, tar etc. Papers should be submitted via e-mail to svv03(a)comp.nus.edu.sg The deadlines are as follows. Submission deadline: September 15, 2003 Notification of Acceptance: October 15, 2003 Final Version submission: November 15, 2003 We plan to publish selected papers from the workshop as Electronic Notes in Theoretical Computer Science (ENTCS). Note that ENTCS papers should be at least 10 pages in ENTCS format. ----------------------- Program Committee -------------------------- Krzysztof R. Apt, CWI (Netherlands) and NUS (Singapore). Giorgio Delzanno, University of Genova (Italy). Maurizio Gabbrielli, University of Bologna (Italy). Shriram Krishnamurthi, Brown University (USA). Andreas Podelski, Max Planck Institute (Germany). C.R. Ramakrishnan, SUNY Stony Brook (USA). Wang Yi, Uppsala University (Sweden). --------------------- Invited Speaker ------------------------ Ramesh Bharadwaj, Naval Research Laboratory (USA). Talk Title: Rigorous Methods for Software Construction: Retrofitting "Engineering" into Software Engineering -------------------------- Organizers ---------------------------- Sandro Etalle, University of Twente, Netherlands. Supratik Mukhopadhyay, NASA IV&V and University of West Virginia, USA. Abhik Roychoudhury, National University of Singapore (Workshop Co-ordinator). ****************************************************

1 0

Re: Circular Instance declarations
by oleg＠pobox.com 08 Sep '03

08 Sep '03

Ashley Yakeley wrote: > Would it be reasonable for the compiler to check back through the > stack and allow the circularity? It will just create an ordinary > recursive function. The following works. Flags: -fglasgow-exts -fallow-undecidable-instances data D r = ZeroD | SuccD (r (D r)) instance (Eq (r (D r))) => Eq (D r) where ZeroD == ZeroD = True (SuccD a) == (SuccD b) = a == b _ == _ = False newtype C a = MkC a instance Eq (C (D C)) where (MkC ZeroD) == (MkC ZeroD) = True (MkC (SuccD a)) == (MkC (SuccD b)) = a == b _ == _ = False equalDC :: D C -> D C -> Bool equalDC = (==) c2 = SuccD (MkC (SuccD (MkC ZeroD))) c1 = SuccD (MkC (ZeroD)) *Main> equalDC c2 c2 True *Main> equalDC c2 c1 False *Main> equalDC ZeroD c1 False *Main> equalDC ZeroD ZeroD True *Main>

1 0

Re: [mercury-users] pragma compiled_memo for compile-time tabled evaluation
by Stefan Karrmann 05 Sep '03

05 Sep '03

André Platzer (Fri, Sep 05, 2003 at 04:03:42PM +0200): > Hello Mercury users! > > Is there any way to extend tabled evaluation to compile-time? As far as > I understand, normal tabled evaluation memorises values computed at > run-time. On an invocation with the same arguments, then mercury reuses > those values instead of a second computation. This is very cool. > > However, I wonder if there is a way to extend this idea to compile-time. > So in case of a constant function like > > %% computes the number pi with a precision of 500 digits. > :- func pi_to_500_digits = string. > :- mode pi_to_500_digits = out is det. > :- pragma memo(pi_to_500_digits/0). > > after compilation, the program will compute pi to 500 digits only at the > first time this constant is used, but repeat this computation for every > program run. An improvement in this situation of constant functions (or > at least functions depending upon arguments of a small finite domain) > would be to perform the respective computation only once, at > compile-time instead of repeatedly at each new program run. The compiler > would evaluate the function at compile-time and store its tabled value > instead of the machine code for performing the computation. How could one balance compile-time computation against space consumption? E.g. (in Haskell - sorry) pi_s_500_digit = pi_to_500_digits !! 500 The space consumption of the result is small, but the computation is expensive. This is a good case for compile-time computation. While enumerate_123456 = [1..123456] consumes much space and minimal time. To decide automatically about compile-time computation we may need a pragma that sets a threshold: :- pragma reductions_per_byte_at_compile_time(10). Store the value in the library if the compiler needs 10 or more reductions per byte of the value. Sincerly, -- Stefan

1 0

Re: Haskell for non-Haskell's sake
by Graham Hutton 05 Sep '03

05 Sep '03

I use Haskell for processing the examination marks of our 900 students. Our University has a system that can do all of this, but to ensure that I understood all the rules and regulations I coded up a simple version in Haskell, which comprises around 400 lines. It takes a CSV (comma separated values) file downloaded from our central marks database, from which five different marks reports can be produced, which are then written out as CSV files for viewing and further processing using Excel. Interesting, this simple Haskell program showed that the University system implemented one of the progression rules incorrectly :-) Graham +---------------------------------------------------------------------+ | Dr Graham Hutton Email : gmh(a)cs.nott.ac.uk | | School of Computer Science and IT Web : www.cs.nott.ac.uk/~gmh | | University of Nottingham | | Jubilee Campus, Wollaton Road | | Nottingham NG8 1BB Phone : +44 (0)115 951 4220 | | United Kingdom Fax : +44 (0)115 951 4254 | +---------------------------------------------------------------------+

5 6

unary minus
by Christian Maeder 05 Sep '03

05 Sep '03

Hi, I wonder why Haskell only allows the unary minus on the left side of an expression ("lexp" in the grammar). There should be no problem to uniquely recognize an unary minus right beside an operation symbol ("qop"). Does the grammar allow two consecutive qops in other cases? This would allow "1 * - 1" to be correct (which I think is sort of "standard"), while "1 - 1" clearly is the infix minus. What was the rational for the current restriction of the unary minus? Do I oversee something? Christian

1 1

Re: proving the monad laws
by oleg＠pobox.com 05 Sep '03

05 Sep '03

Hello! > Would it be possible to write a piece of Haskell code which checks > the monadic laws automatically by simulating evaluation in this way? To some extent, yes. The proof in the previous message was based on normalization, with respect to associative laws and some betas. So we can take (st f) . (st g) and do: - inlining of the 'st' operation - de-sugaring into core Haskell - more inlining and beta [perhaps to a certain depth] - rearranging expression based on associative laws, e.g., converting f . (g . h) into (f . g) . h converting case (case x of P -> A) of P' -> A' into case x of P -> case A of P' -> A' Then do the same for (st ((st f) . g)) and compare the results. If the results are identical, great. Otherwise, the user has to look at the results and decide if they are the same based on his intuition. GHC already does inlining, de-sugaring, and some betas. I think there is a flag that makes GHC dump the result of these operations for normalization with respect associative laws. BTW, GHC accepts user-defined rules: so we can express associativity rules for known operations and direct GHC to normalize terms with respect to these laws. I don't know how to express side conditions though (e.g., the normalization of 'case' above is valid only if the variables bound by pattern P do not occur in P', A'). It would be great if there was a RULES-pragma operation to alpha-rename bound variables in a term. In that case, we can safely normalize more expressions.

1 0