- Haskell - Haskell.org

TACAS 2004 Call For Papers (deadline: October 17)
by AG2 Guest Account 3 13 Sep '03

13 Sep '03

Call for Papers TACAS'04 [http://www.daimi.au.dk/%7Ecpn/tacas04/] Tenth International Conference on Tools and Algorithms for the Construction and Analysis of Systems A member conference of ETAPS 2004 [http://www.lsi.upc.es/etaps04/] European Joint Conferences on Theory and Practice of Software IMPORTANT DATES * October 17, 2003 Submission deadline * December 12, 2003 Notification of authors * January 9, 2004 Camera ready version due * March 29 - April 2, 2004 TACAS 2004 Conference PROGRAM COMMITTEE Jonathan Billington, University of South Australia, Adelaide (Australia) Bernard Boigelot, Université de Liège (Belgium) Ed Brinksma, University of Twente (The Netherlands) Witold Charatonik, University of Wroclaw (Poland) Rance Cleaveland, SUNY Stony Brook (USA) Giorgio Delzanno, Università di Genova (Italy) David L. Dill, Stanford University (USA) Susanna Donatelli, Università degli Studi di Torino (Italy) Javier Esparza, University of Edinburgh (UK) John Hatcliff, Kansas State University (USA) Kurt Jensen (co-chair), University of Aarhus (Denmark) Orna Kupferman, Hebrew University, Jerusalem (Israel) Yassine Lakhnech, Verimag Grenoble (France) Kim Larsen, Aalborg University (Denmark) Anca Muscholl, Université Paris 7 (France) Anna Philippou, University of Cyprus (Cyprus) Andreas Podelski (co-chair), Max-Planck-Institut Saarbrücken (Germany) Jaco van de Pol, CWI Amsterdam (The Netherlands) Jakob Rehof, Microsoft Redmond (USA) Martin C. Rinard, MIT, Cambridge (USA) Bill Roscoe, Oxford University (UK) Bernard Steffen, Universität Dortmund (Germany) Ofer Strichman, Carnegie Mellon University, Pittsburgh (USA) Antti Valmari, Tampere University of Technology (Finland) Andreas Zeller, Universität des Saarlandes (Germany) CONFERENCE DESCRIPTION TACAS is a forum for researchers, developers and users interested in rigorously based tools for the construction and analysis of systems. The conference serves to bridge the gaps between different communities --- including but not limited to those devoted to formal methods, software and hardware verification, static analysis, programming languages, software engineering, real-time systems, and communications protocols --- that share common interests in, and techniques for, tool development. In particular, by providing a venue for the discussion of common problems, heuristics, algorithms, data structures and methodologies, TACAS aims to support researchers in their quest to improve the utility, reliability, flexibility and efficiency of tools for building systems. TACAS is a member conference of the European Joint Conferences on Theory and Practice of Software (ETAPS), which is the primary European forum for academic and industrial researchers working on topics relating to Software Science. ETAPS 2004 [http://www.lsi.upc.es/etaps04/] is the seventh joint conference in this series. The conference is organized by the Technical University of Catalonia (UPC) [http://www.upc.es] Tool descriptions and case studies with a conceptual message and theoretical papers with a clear link to tool construction are all encouraged. The specific topics covered by the conference include, but are not limited to, the following: * Specification and verification techniques * Theorem-proving and model-checking * System construction and transformation techniques * Static and run-time analysis * Compositional and refinement-based methodologies * Testing and test-case generation * Analytical techniques for real-time, hybrid and safety-critical systems * Tool environments and tool architectures * Applications and case studies As TACAS addresses a heterogeneous audience, potential authors are strongly encouraged to write about their ideas in general and jargon-independent, rather than application- and domain-specific, terms. Authors reporting on tools or case studies are strongly encouraged to indicate how their experimental results can be reproduced and confirmed independently. TACAS 2003 received a *record number of submissions*: 140 research papers and 20 tool papers were submitted. The Program Committee selected 35 research papers and 6 tool papers, and invited 2 research paper submissions as tool papers. The average acceptance ratio was 27% (25% for research papers and 30% for tool papers). * Conference program 2003 [http://www.inrialpes.fr/vasy/tacas03/program.html] * On-line proceedings 2003 [http://link.springer.de/link/service/series/0558/tocs/t2619.htm] (available via Springer's LINK service) PROGRAM COMMITTEE CHAIRS Kurt Jensen, University of Aarhus (Denmark) [http://www.daimi.au.dk/~kjensen/] Andreas Podelski, Max-Planck-Institut Saarbrücken (Germany) [http://www.mpi-sb.mpg.de/~podelski] TOOL CHAIR Bernhard Steffen, Universität Dortmund (Germany) [http://ls5-www.cs.uni-dortmund.de/staff/steffen.de.html] INVITED SPEAKER Antti Valmari, Tampere University of Technology (Finland) [http://www.cs.tut.fi/~ava/] ------------------------------------------------------------------------ SUBMISSION GUIDELINES As with other ETAPS conferences, TACAS accepts two types of contributions: *research papers* and *tool demonstration papers*. Both types of contributions will appear in the proceedings and have oral presentations during the conference. Please notice that there are *two different conference services* for submission of papers: * The TACAS 2004 Conference Service is used for submission of research papers. * The TACAS 2004 TOOL Conference Service is used for submission of tool demonstration papers. -- Authors who anticipate possible last minute delays in the submission of a full research paper or a full tool demonstration paper are encouraged to submit a title and abstract well in advance of the deadline. -- Research papers Research papers cover one or more of the topics above, including tool development and case studies from a perspective of scientific research. Research papers are evaluated by the TACAS Program Committee. Submitted research papers *must*: * be in English and have a maximum of 15 pages, * present original research which is unpublished and not submitted elsewhere (conferences or journals) -- in particular, simultaneous submission of the same contribution to multiple ETAPS conferences is forbidden, * use the Springer-Verlag LNCS style [http://www.springer.de/comp/lncs/authors.html] * be submitted electronically in Postscript or PDF form via the TACAS 2004 Conference Service no later than October 17. Submissions deviating from these instructions may be rejected without review. Any questions regarding this policy should be directed to the Program Committee Chairs Kurt Jensen [http://daimi.au.dk/~kjensen/] or Andreas Podelski [http://www.mpi-sb.mpg.de/~podelski] prior to submitting. Tool demonstration papers Tool demonstration papers present tools based on aforementioned technologies (e.g., theorem-proving, model-checking, static analysis, or other formal methods) or fall into the above application areas (e.g., system construction and transformation, testing, analysis of real-time and hybrid systems, etc.). Tool demonstration papers are evaluated by the TACAS Tool Chair with the help of the Program Committee. Submitted tool demonstration papers *must*: * be in English and have a maximum of 4 pages, * have an appendix (not included in the 4 page count) that provides a detailed description of: o how the oral presentation will be conducted, e.g. illustrated by a number of snapshots, o the availability of the tool, the number and types of users, other information which may illustrate the maturity and robustness of the tool, o link to a web-page for the tool (if this exists). The appendix will *not* be included in the proceedings, but during the evaluation of the tool demonstration papers it will be *equally important* as the pages for the proceedings * use the Springer-Verlag LNCS style [http://www.springer.de/comp/lncs/authors.html] * be submitted electronically in Postscript or PDF form via the TACAS 2004 TOOL Conference Service no later than October 17. Submissions deviating from these instructions may be rejected without review. Any questions regarding this policy should be directed to the Tool Chair Bernhard Steffen [http://ls5-www.cs.uni-dortmund.de/staff/steffen.de.html]

1 0

Where are higher-rank and existential types used?
by Ken Shan 13 Sep '03

13 Sep '03

Hello, Norman Ramsey and I are looking for examples of where higher-rank polymorphism and existential types are useful. Can anyone think of uses besides the following? Higher-rank types are used in: - Deforestation Andrew Gill, John Launchbury, and Simon L. Peyton Jones. 1993. A short cut to deforestation. In _Functional programming languages and computer architecture: 6th conference_, 223-232. New York: ACM Press. - Lazy functional state threads John Launchbury and Simon L. Peyton Jones. 1994. Lazy functional state threads. In _PLDI '94: Proceedings of the ACM conference on programming language design and implementation_, vol. 29(6) of _ACM SIGPLAN Notices_, 24-35. New York: ACM Press. - Generic (polytypic) programming Ralf Hinze. 2000. A new approach to generic functional programming. In _POPL '00: Conference record of the annual ACM symposium on principles of programming languages_, 119-132. New York: ACM Press. Ralf Lämmel and Simon L. Peyton Jones. 2003. Scrap your boilerplate: A practical design pattern for generic programming. In _Proceedings of the 2003 ACM SIGPLAN international workshop on types in languages design and implementation_, 26-37. New York: ACM Press. - Data type invariants Chris Okasaki. 1999. From fast exponentiation to square matrices: An adventure in types. In _ICFP '99: Proceedings of the ACM international conference on functional programming_, vol. 34(9) of _ACM SIGPLAN Notices_, 28-35. New York: ACM Press. Ralf Hinze. 2001. Manufacturing datatypes. _Journal of Functional Programming_ 11(5): 493-524. Richard Bird and Ross Paterson. 1999. de Bruijn notation as a nested datatype. _Journal of Functional Programming_ 9(1): 77-91. Existential types are used in: - Object-oriented programming Benjamin C. Pierce and David N. Turner. 1994. Simple type-theoretic foundations for object-oriented programming. _Journal of Functional Programming_ 4(2): 207-247. Konstantin Läufer. 1996. Type classes with existential types. _Journal of Functional Programming_ 6(3): 485-517. - Abstract data types John C. Mitchell and Gordon D. Plotkin. 1988. Abstract types have existential type. _ACM Transactions on Programming Languages and Systems_ 10(3): 470-502. Any pointers or technique descriptions would be highly appreciated! If there are many contributions, I will post an updated version of this list. Ken -- Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig United Nations Day is 24 October. http://www.un.org/events/unday/ The Lost Voice of Radio Beijing http://www.milinfoserv.net/lvrb.html Write letters! We got half of New Testament that way.

2 1

File reading question
by Gordon James Miller 12 Sep '03

12 Sep '03

Hello all, I believe I have a mental block on some issues related to IO and would really appreciate some help on this. I have a text file that contains two columns of numbers, basically X and Y values. I need a function (or set of functions) that reads this file and returns two arrays, one of the X values and one of the Y. A sample data file might look like. 10.0 20.0 20.0 40.0 30.0 60.0 40.0 80.0 Reading in this file should return two arrays [10.0, 20.0, 30.0, 40.0] and [20.0, 40.0, 60.0, 80.0]. Thanks for any help on this, I just don't seem to get IO in Haskell without reassignments. Gordon James Miller Promisemark, Inc. Senior Computer Scientist gmiller(a)promisemark.com (571)330-9012 The box said "Requires Windows 95 or better." So I installed LINUX

3 2

Syntax extensions (was: RE: The Future of Haskell discussion at the Haskell Workshop)
by Simon Marlow 11 Sep '03

11 Sep '03

> > I also think that having backwards compatability is not much of an > > issue. After all, ghc has introduces a number of not backward > > compatable changes to haskell, and I never heard any complaints. > > Oh no? > > Implicit parameters: I'm sure it is a great thing, but I'd already > used the (?) operator, and need -fglasgow-exts. Now my program > depends on a bunch of well places spaces to compile. > > Template Haskell: really cool new feature, which just happens to use > a syntax that overlaps with the list comprehension syntax. > > And now, let's just screw any backwards compatibility, and re-engineer > the records system¹. We at GHC HQ agree, and for future extensions we'll move to using separate options to enable them rather than lumping everything into -fglasgow-exts. This is starting to happen already: we have -farrows, -fwith, -fffi (currently implied by -fglasgow-exts). Of course, if we change the language that is implied by -fglasgow-exts now, we risk breaking old code :-) Would folk prefer existing syntax extensions be moved into their own flags, or left in -fglasgow-exts for now? I'm thinking of: - implicit parameters - template haskell - FFI - rank-N polymorphism (forall keyword) - recursive 'do' (mdo keyword) Cheers, Simon

8 7

GHC code generation
by Graham Klyne 11 Sep '03

11 Sep '03

In an exchange of ideas with a friend, this question arose: [[ I've been looking at GHC, and it looks like it has generates machine code directly rather than via C--. I know that Simon Peyton Jones (famous in the Haskell world) is one of the authors of C--, but I can find no direct connection between this and GHC or Haskell. Have you any idea where I might find this connection? ]] In my discussion with him, I had assumed that GHC generates code via C-- and a version of the GCC compiler (why else is GCC part of the GHC installation?). Can anyone shed any light or pointers? Thanks. #g ------------ Graham Klyne GK(a)NineByNine.org

3 2

The Future of Haskell discussion at the Haskell Workshop
by nilsson＠cs.yale.edu 11 Sep '03

11 Sep '03

Dear Haskellers, This year's Haskell Workshop, held in Uppsala as a part of PLI, traditionally concluded with a discussion on the future of Haskell. This time an attempt was made to structure the discussion a little bit by focusing on two specific topics, and by having each topic being introduced by a short presentation. The first topic was Haskell records, introduced by Simon Peyton Jones, Microsoft Research, Cambridge, UK. The second topic was GUI libraries for Haskell, introduced by Axel Simon, the University of Kent, UK. While the current Haskell record system, or rather support for labeled fields, is vastly superior to not having any record facility at all, and appealing due to its simplicity and not incurring any run-time penalty, most people would agree that it does leave a lot be desired. However, they would not necessarily agree on exactly what is to be desired: the design space is quite large, and it is not easy to evaluate how useful various record features would be in practice, and if the cost in terms of increased language complexity and backwards compatibility issues is warranted. Unsurprisingly, opinions expressed during the discussion were rather divided. In the end, it seemed that the fact that the present system, despite its faults, is simple and has proved to be useful convinced a majority of the people present that if the system were to be improved, it should only be rather modest improvements that would not break backward compatibility. For example, one of the most annoying limitations of the present system is that record labels have to be distinct. Maybe this restriction could be lifted without sacrificing compatibility. Here is how Simon Peyton Jones summarized the discussion: The conclusion I took away was this There are undoubted advantages to having better records, but (a) they all make the language more complicated (b) there are many possible design choices (not only has/lacks, but also record concatenation, length vs depth subtyping, and more I'm sure) (c) they almost certainly conflict with existing programs (d) the existing system is really not too bad That all argues for the status quo. I did have a conversation with Peter Thiemann afterwards. We discussed a record system which is an upward compatible extension of what we have now, though less powerful than the variants I have previously proposed. * Records are not anonymous. e.g. {x::Int, y::Bool} is not a type They are declared exactly as now, so that data T = T { x::Int, y::Bool } declares a type T. * However, you can have more than one record with the same field name. So the field selectors are overloaded, much as with has-predicates x :: (t has x::a) => t -> a * So a function like f v = v.x + v.y would get the inferred type f :: (t has x::a, t has y::a, Num a) => t -> a * Also retain Haskell's existing record construction and update syntax could be possible. The GUI library discussion focused on questions such as what exactly are the desirable properties of such a library. For example, to what extent is it necessary that applications are able to adopt the look-and-feel of the platform on which they happen to be running. Related to this was the question of whether to focus efforts on a Common GUI API (CGA) that would allow applications to adapt to specific platforms, or whether it would be sufficient to go for something based on an existing cross-platform API, such as wxWindows, even if that meant violating certain look-and-feel aspects on certain platforms, and inability to access platform-specific functionality. Axel Simon has promised to e-mail a more complete record of the GUI-part of the discussion shortly. All the best, /Henrik -- Henrik Nilsson Yale University Department of Computer Science nilsson(a)cs.yale.edu

13 26

Circular Instance Declarations
by Ashley Yakeley 11 Sep '03

11 Sep '03

When -fallow-undecidable-instances is switched on, is there any reason why circular instances are forbidden? For instance: module CircularInsts where { 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 deriving Eq; equalDC :: D C -> D C -> Bool; equalDC = (==); } When I compile this, I get this: $ ghc -fglasgow-exts -fallow-undecidable-instances -c CircularInsts.hs CircularInsts.hs:2: Context reduction stack overflow; size = 21 Use -fcontext-stack20 to increase stack size to (e.g.) 20 `Eq (C (D C))' arising from use of `==' at CircularInsts.hs:16 `Eq (D C)' arising from use of `==' at CircularInsts.hs:16 `Eq (C (D C))' arising from use of `==' at CircularInsts.hs:16 `Eq (D C)' arising from use of `==' at CircularInsts.hs:16 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. -- Ashley Yakeley, Seattle WA

4 8

Re: Syntax extensions (was: RE: The Future of Haskell discussion at the Haskell Workshop)
by Graham Klyne 11 Sep '03

11 Sep '03

At 13:13 10/09/03 +0100, Simon Marlow wrote: >Of course, if we change the language that is implied by -fglasgow-exts >now, we risk breaking old code :-) Would folk prefer existing syntax >extensions be moved into their own flags, or left in -fglasgow-exts for >now? I'm thinking of: > > - implicit parameters > - template haskell > - FFI > - rank-N polymorphism (forall keyword) > - recursive 'do' (mdo keyword) My 2p is that extensions that might be regarded as "mainstream" would usefully be included in a single easy-to-use switch like -fglasgow-exts. I think the only part I use from the above list is rank-N polymorphism, and that is imported from useful libraries. Where do multi-parameter classes fit in? #g ------------ Graham Klyne GK(a)NineByNine.org

2 1

Request for Instances
by Brandon Michael Moore 10 Sep '03

10 Sep '03

Hi everyone. I've been looking at the restrictions on instances in the H98 standard and thinking about alternatives. I would like to have a body of data type and class/instance declarations so I can test how useful various extensions would be. Please send or direct me to code that requires -fallow-undecidabe-instances. Thanks. Brandon

1 0

Type Class Problem
by Brandon Michael Moore 10 Sep '03

10 Sep '03

Hello everyone I think I'm close to useful results on the instance restrictions. First there's an obvious extension to the Haskell98 rule. The H98 rule says the instance head must be a type constructor applied to type variables, and the context must mention only those type variables. This gives a termination proof by counting constructors. If the rule is weakened to allow an arbitrary type expression in the head and require that the context mention only strict subexpressions of the head, the same proof still applies. I'm not sure how useful this is, but we might as well allow it. Second, I have half a result in the direction of allowing the context to mention types that arise from applying type constructors used in the instance head. This requires accepting regular derivations, which means the compiler would need to track all previous goals while deriving an instance, and handle a second occurance of a goal by producing a reference to the dictionary for the first occurance (which may not be constructed yet), rather than blindly continuing the derivation. First I will explain the proof method. It's related to structural induction, but not quite the same. Suppose we have a subexpression relation on type expressions such that every type expression has only a finite number of subexpressions. If instance contexts only mention subexpressions of the head, then searching for an instance for a type can only generate #of subexpressions*#of classes distinct goals. Therefore, in finite time either the derivation will fail, or we will product a regular derivaiton. Alternately, we only try to derivive an instance the first time it arises as a goal, so each time we apply an instance rule there is one less goal in the pool of possible goals, which must eventually be exhausted. The syntactic subexpression relation obviously has these properties, but it's often useful to refer to types that show up when we apply type constructors. For example, my case and a simplification of Ashley's: data Mu f = In (f (Mu f)) instance C (f (Mu f)) => C (Mu f) On the other hand, we can't unfold all type constructors because some types are irregular, or, we encounter an infinite number of types while expanding the type constructors. Define a kind indexed family of predicates on type constructors, R_K(T), where the property is true if T::K, T is regular (including expanding the insides of lambdas), and if K=K1->K2, then R_K2(T t) for all t such that R_K1(t). Say a type is regularity preserving if it satisfies the predicate corresponding to its kind. Any type expression build entirely from regularity preserving type constructors will be regular. I think that a subexpression relation that allows expanding applications regularity preserving type constructors will give any type a finite number of subexpressions, but I don't know enough about the structure of regularity preserving type constructors to prove it. The missing half here is an algorithm for testing whether a type constructor is regularity preserving. For this the body of the type constructor can be simplified to consist of just the type constructor applications in the body. Apply the type constructor to skolem arguments, and check whether the resulting tree is regular. I don't know how to do this. Another approach is to draw out a dependency graph between type constructors, with an edge from A to B for each use of B in the definition of A, labeled with the arguments used. Then the question is whether starting from out type applied to tyvars we can find some path through the graph that generates an infinite number of types, where we keep track of the current node and the current arguments, and modify the arguments as directed by a label when moving along an edge. I don't know if the search can even a tail repeating path that witnesses the irregularity, let alone a family of paths that can be tested. Any assistance here would be appreciated. Thanks Brandon

1 0