September 2003 - Haskell

Position at Galois
by Andy Moran 10 Sep '03

10 Sep '03

Hi all, Galois has a position open for someone who has good FP skills, is experienced with compilers of all kinds, and wants to live in wonderful Portland, otherwise known as the Greatest Place On Earth To Live. Galois is a small company, started in late 1999 by John Launchbury, Andy Gill, Jeff Lewis, and me. We use functional languages (mainly Haskell) and programming language design techniques (abstract modelling, abstract interpretation, program analysis, etc.) to develop high assurance software for a variety of U.S. government and industrial clients. Basically, we got sick of complaining about industry not using all our (*) great ideas, and decided to start using them ourselves. If you're interested, please send your resume to jobs(a)galois.com. Cheers, Andy (*) The Haskell community, and the wider programming language design and semantics community. -- Andy Moran Ph. (503) 626 6616, x113 Galois Connections Inc. Fax. (503) 350 0833 12725 SW Millikan Way, Suite #290 http://www.galois.com Beaverton, OR 97005 moran(a)galois.com

1 0

RE: The Future of Haskell discussion at the Haskell Workshop
by Gregory Morrisett 09 Sep '03

09 Sep '03

Coming from the ML world, I can say that I find the lack of proper records a real loss. It is extremely convenient to write functions which take many parameters as taking a record, for then you don't have to worry so much about the order of arguments. SML gets this much right, but the ad hoc treatment of record selection in SML is a royal pain. Haskell has all of the machinery needed to support this nicely so it seems a shame for it to be omitted. I can say from experience that forcing records to be declared (as in Ocaml) so that there is at most one record type that a given label can come from in any given scope is a royal pain. You're then forced to come up with unique names for the labels so that you don't get a conflict (much as we have to do with datatype constructors.) In Ocaml, you tend to get around this by putting the record types in different modules, but this is only marginally better namespace control. Neither SML nor Ocaml supports polymorphic record selection which is absolutely crucial. I've found few needs for extension or polymorphic update, though there are some compelling examples, and I suspect that more will crop up if these features are widely available. Finally, it seems that good record support at the core level is a nice stepping stone to (first-class) modules. -Greg

1 0

Formal Methods for Components and Objects 2003
by M.M. Bonsangue 09 Sep '03

09 Sep '03

(We apologize for the reception of multiple copies) *********************** CALL FOR PARTICIPATION ********************** Second International Symposium on Formal Methods for Components and Objects (FMCO 2003) DATES 4 - 7 November 2003 PLACE Lorentz Center, Leiden University, Leiden, The Netherlands URL http://fmco.liacs.nl/fmco03.html >>>>>> EARLY REGISTRATION DEADLINE (15/09/2004) IS APPROACHING <<<<< OBJECTIVES The objective of this symposium is to bring together researchers and practioners in the areas of software engineering and formal methods to discuss the concepts of reusability and modifiability in component-based and object-oriented software systems. FORMAT The symposium is a four days event in the style of the former REX workshops, organised to provide an atmosphere that fosters collaborative work, discussions and interaction. The program consists of keynote and technical presentations, and contains an exquisite social event. Speakers' contributions will be published after the symposium in Lecture Notes in Computer Science by Springer-Verlag. PRELIMINARY PROGRAM TUESDAY 4th, November 2003 8:45 - 9:00 Welcome 9:00 - 10:00 Keynote: David Parnas (University of Limerick, IE) Mathematical Documentation of Software 10:00 - 10:30 Break 10:30 - 11:15 Razvan Diaconescu (IMAR, RO) Behavioural specification for hierarchical object composition 11:15 - 12:00 Heike Wehrheim (University of Oldenburg, DE) Preserving Properties under Change 12:00 - 13:30 Lunch break 13:30 - 14:30 Keynote: Andrew D. Gordon (Microsoft Research Cambridge, UK) Formal Tools for Securing Web Services 14:30 - 15:00 Break 15:00 - 15:45 Jeannette Wing (Carnegie Mellon University, USA) Vulnerability Analysis Using Attack Graphs 15:45 - 16:00 Break 16:00 - 16:45 Albert Benveniste (IRISA/INRIA - Rennes, FR) Heterogeneous reactive systems formal modeling 16:45 - 17:30 Yassine Lakhnech (University of Grenoble, FR) t.b.a. WEDNSDAY 5th, November 2003 9:00 - 10:00 Keynote: Tony Hoare (Microsoft Research Cambridge, UK) The Verifying Compiler: a Grand Challenge for Computing Research 10:00 - 10:30 Break 10:30 - 11:15 Willem-Paul de Roever (University of Kiel, DE) Data Refinement: model-oriented proof methods and their comparison 11:15 - 12:00 Frank de Boer (CWI, Amsterdam, NL) Hoare Logics for Object-Oriented Programming: State of the Art 12:00 - 13:30 Lunch break 13:30 - 14:15 Jean-Marc Jezequel (IRISA, Rennes, FR) Model-Driven Engineering: Basic Principles and Open Problems 14:15 - 15:00 Jan Friso Groote (Eindhoven University of Technology, NL) t.b.a. 17:00 - 19:15 Social Event 19:30 - Dinner THURSDAY 6th, November 2003 9:00 - 10:00 Keynote: Yuri Gurevich (Microsoft Research Redmond, USA) The Semantics of AsmL 10:00 - 10:30 Break 10:30 - 11:15 Egon Boerger (Pisa University, IT) Exploiting the "A" in Abstract State Machines for Specification Reuse. A Java/C# Case Study. 11:15 - 12:00 Werner Damm (University of Oldenburg, DE) t.b.a. 12:00 - 13:30 Lunch break 13:30 - 14:30 Keynote: Desmond D'Souza (Kinetium, Austin, USA) t.b.a. 14:30 - 15:00 Break 15:00 - 15:45 Rob van Ommering (Philips Research Laboratories, Eindhoven, NL) Component Based Architectures and Formalization 15:45 - 16:30 Jose Luiz Fiadeiro (University of Leicester, UK) CommUnity on the move: architectures for distribution and mobility 16:30 - 16:45 Break 16:45 - 17:30 Gregor Engels (University of Paderborn, DE) Consistent interaction of components FRIDAY 7th, November 2003 9:00 - 10:00 Keynote: E. Allen Emerson (The University of Texas at Austin, USA) Model Checking Many Components 10:00 - 10:30 Break 10:30 - 11:15 Amir Pnueli (The Weizmann Institute of Science, ISR) t.b.a. 11:15 - 12:00 Natalia Sidorova (Eindhoven University of Technology, NL) Practical approaches for the verification of asynchronous components: model checking, abstraction and static analysis 12:00 - 13:30 Lunch break 13:30 - 14:30 Keynote: Joseph Sifakis (Verimag, FR) t.b.a. 14:30 - 15:00 Break 15:00 - 15:45 Philippe Schnoebelen (CNRS, Cachan, FR) The Verification of Lossy Channel Systems 15:45 - 16:30 Bengt Jonsson (Uppsala University, SE) t.b.a. 16:30 - 17:15 Jan Rutten (CWI, Amsterdam, NL) A case study in coinductive stream calculus: signal flow graphs for dummies MOBI-J WORKSHOP On Monday 3rd, November 2003, there will be a one-day Mobi-J workshop on "Assertional Methods for Java and its Extension with Mobile Asynchronous Channels". REGISTRATION Participation is limited to about 80 people, using a first-in first-served policy. To register, please fill in the registration form at http://fmco.liacs.nl/fmco03.html. The EARLY registration fee (BEFORE September 15, 2003) is 375 euro for regular participants and 250 euro for students It includes the participation to the symposium, a copy of the proceedings, all lunches and refreshments, and a social event (with dinner). ORGANIZING COMMITTEE F.S. de Boer (CWI and Utrecht University) M.M. Bonsangue (LIACS-Leiden University) S. Graf (Verimag) W.P. de Roever (CAU) For more information about participation and registration see the FMCO site above or consult either F.S. de Boer (frb(a)cwi.nl) or M.M. Bonsangue (marcello(a)liacs.nl)

1 0

ANNOUNCE: HOpenGL 1.05 released
by Sven Panne 09 Sep '03

09 Sep '03

HOpenGL, a Haskell binding for OpenGL and GLUT version 1.05 I am pleased to announce the sixteenth release of the Haskell binding for GL 1.2.1 / GLU 1.3 / GLUT 3.7beta. It offers easy access to *the* industrial strength 3D graphics API and a GUI toolkit. More details about HOpenGL can be found at http://haskell.org/HOpenGL/ This is a compatibility/bug fix release with the following changes: * Fixed a memory allocation bug for GL state queries. * Works with new hierarchical libraries now. * Always use the correct calling convention. * The build system works with recent versions of GHC and GreenCard now. As always, feedback and/or patches are highly welcome. A note for people on the bleeding edge: If you are interested in the future of HOpenGL and its new API, you might wish to build GHC from CVS, configuring with `--enable-hopengl'. This will result in a GHC with two additional packages `OpenGL' and `GLUT'. The APIs have improved quite a bit and are now modeled around the notion of state variables. Furthermore, OpenGL's extension mechanism is now supported on all major platforms, including Linux, Windows and Mac OS X. Note that this is still work in progress, but early feedback would be very useful. Have fun! Sven

1 0

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

08 Sep '03

> It looks interesting. Where can I download and try > it? Oops. I forget to post the url. http://htoolkit.sourceforge.net __________________________________ Do you Yahoo!? Yahoo! SiteBuilder - Free, easy-to-use web site design software http://sitebuilder.yahoo.com

1 0

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

08 Sep '03

--- Martin Norb�ck <d95mback(a)dtek.chalmers.se> wrote: > m�n 2003-09-08 klockan 21.21 skrev Krasimir Angelov: > > 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. > > > Krasimir > > It looks interesting. Where can I download and try > it? > > Regards, > > Martin > > ATTACHMENT part 2 application/pgp-signature name=signature.asc __________________________________ Do you Yahoo!? Yahoo! SiteBuilder - Free, easy-to-use web site design software http://sitebuilder.yahoo.com

1 0

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