November 2004 - Haskell

Symposium on Principles of Programming Languages 2005: Call for Participation
by David Walker 26 Nov '04

26 Nov '04

POPL 2005 Call for Participation 32nd Annual ACM SIGPLAN - SIGACT Symposium on Principles of Programming Languages Long Beach, California January 12-14, 2005 http://www.cs.princeton.edu/~dpw/popl/05/ Scope of the Conference The annual Symposium on Principles of Programming Languages is a forum for the discussion of fundamental principles and important innovations in the design, definition, analysis, transformation, implementation and verification of programming languages, programming systems, and programming abstractions. Important Dates * Hotel reservation deadline: December 21, 2004 * Reduced fees deadline: December 30, 2004 (11:59 PM, EST USA) - Register at http://www.regmaster.com/popl2005.html * Main conference: January 12-14, 2005. * Affiliated events: January 10-11 and January 15, 2005 Invited Speakers * Pat Hanrahan (Stanford University) * Rob Pike (Google): Interpreting the Data * Peter Selinger (University of Ottawa): Programming Languages for Quantum Computing Location & Hotel The POPL 2005 conference site is Hyatt Regency Long Beach, 200 South Pine Avenue, Long Beach, CA. Complete information concerning how to book rooms and travel to Long Beach may be found at the conference web site (http://www.cs.princeton.edu/~dpw/popl/05/) The Hyatt Regency is right next to a variety of entertainment areas, including the Shoreline Village, the Rainbow Harbor, and the Shoreline Marina, which offer sport fishing, boat rentals, personal boat rentals, shopping, great food and other diversions. For those wishing to take in some sun this January, one can walk east from the hotel, about a 1/4 mile, along the Shoreline Marina, to a large, sandy, public beach. In addition, the remarkable Aquarium of the Pacific, which houses more than 12,500 animals and offers the possibility of coming face-to-face or even touching the world's greatest predators, is only a 1/4 mile west. On Thursday January 13th, we will be having a tour and banquet on the Queen Mary ocean liner. Be sure to reserve your room by December 21st, 2004 and register for the conference by December 30th, 2004. Program Wednesday, Jan 12 8:30AM -- 9:30AM: Invited talk: Interpreting the Data, Rob Pike (Google) 10AM Session: * Associated Types with Class - Manuel Chakravarty, Gabriele Keller, Simon Peyton-Jones, Simon Marlow * Environmental Acquisition Revisited - Richard Cobbe, Matthias Felleisen * Polymorphic Bytecode: Compositional Compilation for Java-like Languages - Davide Ancona, Ferrucio Damiani, Sophia Drossopoulou, Elena Zucca * A Simple Typed Intermediate Language for Object-Oriented Languages - Juan Chen, David Tarditi 1:30PM Session: * Parametric Polymorphism for XML - Haruo Hosoya, Alain Frisch, Giuseppe Castagna * A Bisimulation for Type Abstraction and Recursion - Eijiro Sumii, Benjamin Pierce * A Syntactic Approach to Eta Equality in Type Theory - Healfdene Goguen * Slot Games: A Quantitative Model of Computation - Dan Ghica 4PM Session: * Synthesis of Interface Specifications for Java Classes - Rajeev Alur, Pavol Cerny, P. Madhusudan, Wonhong Nam * Dynamic Partial-Order Reduction for Model Checking Software - Cormac Flanagan, Patrice Godefroid * Proof-Guided Underapproximation-Widening for Multi-Process Systems - Orna Grumberg, Flavio Lerda, Ofer Strichman, Michael Theobald * Transition Predicate Abstraction and Fair Termination - Andreas Podelski, Andrey Rybalchenko 6PM: Business meeting / PC report Thursday, Jan 13 8:30AM: Invited talk: Programming Languages for Quantum Computing, Peter Selinger (University of Ottawa) 10AM Session: * Communicating Quantum Processes - Simon Gay, Rajagopal Nagarajan * Downgrading Policies and Relaxed Noninterference - Peng Li, Steve Zdancewic * A Probabilistic Language Based Upon Sampling Functions - Sungwoo Park, Frank Pfenning, Sebastian Thrun * Mutatis Mutandis: Safe and Predictable Dynamic Software Updating - Gareth Stoyle, Michael Hicks, Gavin Bierman, Peter Sewell, Iulian Neamtiu 1:30PM Session: * Transactors: A Programming Model for Maintaining Globally Consistent Distributed State in Unreliable Environments - John Field, Carlos Varela * Theoretical Foundations for Compensations in Flow Composition Languages - Roberto Bruni, Hernan Melgratti, Ugo Montanari * From Sequential Programs to Multi-Tier Applications by Program Transformation - Matthias Neubauer, Peter Thiemann * Combinators for Bi-Directional Tree Transformations: A Linguistic Approach to the View Update Problem - Nathan Foster, Michael Greenwald, Jonathan Moore, Benjamin Pierce, Alan Schmitt 4:30PM: Tour and conference dinner on the Queen Mary ocean liner Friday, Jan 14 8:30AM: Invited talk, Pat Hanrahan (Stanford University) 10AM Session: * Separation Logic and Abstraction - Matthew Parkinson, Gavin Bierman * Permission Accounting in Separation Logic - Richard Bornat, Cristiano Calcagno, Peter O'Hearn, Matthew Parkinson * Context Logic and Tree Update - Cristiano Calcagno, Philippa Gardner, Uri Zarfaty * Connecting Effects and Uniqueness with Adoption - John Tang Boyland, William Retert 1:30PM Session: * A Semantics for Procedure-Local Heaps and its Abstractions - Noam Rinetzky, Jörg Bauer, Thomas Reps, Mooly Sagiv, Reinhard Wilhelm * Region-Based Shape Analysis with Tracked Locations - Brian Hackett, Radu Rugina * Precise Interprocedural Analysis using Random Interpretation - Sumit Gulwani, George Necula * Numeric Analysis of Array Operations - Denis Gopan, Thomas Reps, Mooly Sagiv 4PM Session: * Scalable Error Detection using Boolean Satisfiability - Yichen Xie, Alex Aiken * Automated Soundness Proofs for Dataflow Analyses and Transformations via Local Rules - Sorin Lerner, Todd Millstein, Erika Rice, Craig Chambers * The Java Memory Model - Jeremy Manson, William Pugh, Sarita Adve Program Chair: Martín Abadi University of California, Santa Cruz Computer Science Department Santa Cruz, CA 95064 E-mail: abadi(a)cs.ucsc.edu General Chair: Jens Palsberg University of California, Los Angeles Computer Science Dept, 4531K Boelter Hall, Los Angeles, CA 90095 Phone: 310-825-6320 Fax: 310-794-5057 E-mail: palsberg(a)ucla.edu Program Committee: Martín Abadi, UC Santa Cruz (chair) Rastislav Bodik, UC Berkeley Perry Cheng, IBM (T.J. Watson Research Center) William Cook, UT Austin Michael Ernst, MIT Giorgio Ghelli, Università di Pisa Yossi Gil, Technion Ralf Hinze, Universität Bonn Martin Hofmann, Ludwig-Maximilians-Universität München Alan Jeffrey, Bell Labs, Lucent / DePaul University Andrew Kennedy, Microsoft Research (Cambridge) Naoki Kobayashi, Tohoku University Julia Lawall, University of Copenhagen Andrew Myers, Cornell University Gordon Plotkin, University of Edinburgh François Pottier, INRIA (Rocquencourt) Sriram Rajamani, Microsoft Research (Redmond) John Reppy, University of Chicago Zhong Shao, Yale University Henny Sipma, Stanford University Treasurer: Manuel Fähndrich Publicity: David Walker

1 0

Bandwidth
by Nick Benton 26 Nov '04

26 Nov '04

Genuinely inspiring though it is to observe the vitality of the Haskell community, especially by comparison with we taciturn SML folks, recent discussions on top-level initialization etc. have got a bit high-bandwidth for the casual lurker. I really don't want to unsubscribe, so might I politely, respectfully and gently reiterate Simon's request that such skirmishes move to Haskell Café after the first few volleys have been exchanged? That's what it's there for. Peace and purity, Nick -----Original Message----- From: haskell-bounces(a)haskell.org [mailto:haskell-bounces@haskell.org] On Behalf Of Graham Klyne Sent: 26 November 2004 11:27 To: Lennart Augustsson Cc: The Haskell Mailing List Subject: Re: [Haskell] A puzzle and an annoying feature At 19:14 25/11/04 +0100, Lennart Augustsson wrote: >Graham Klyne wrote: >>I have a concern with this, if I understand the issue correctly. >>Suppose I have a source module that compiles and runs correctly. >>Now suppose I add a restricted (selective) import statement to the file, >>explicitly introducing a name that I know does not clash with anything in >>my module. I expect the module to continue to compile and run correctly. >>If I understand Lennart's proposal correctly, adding such an import could >>cause the compilation to fail, by adding new instance options that then >>needs to be disambiguated. >Not in my particular case. The class is local to the module. Any >instance declaration would have to be in that module. OK, I missed that. But, it seems to me, that adding export of the class concerned to the module heading could raise a similar scenario to that mentioned. It's less clear-cut, but it seems surprising to me that the choice of whether or not to export something from a module should (potentially) change its meaning or validity. #g ------------ Graham Klyne For email: http://www.ninebynine.org/#Contact _______________________________________________ Haskell mailing list Haskell(a)haskell.org http://www.haskell.org/mailman/listinfo/haskell

1 0

A puzzle and an annoying feature
by Lennart Augustsson 26 Nov '04

26 Nov '04

Here is a small puzzle. -- The following generates a type error: f :: Char -> Char f c = let x = g c in h x -- But this definition does not: f :: Char -> Char f c = let x :: Bool x = g c in h x Furthermore, replacing Bool by any other type in the latter definition will always give a type error. How is this possible? Scroll down for the answer. Here is the module: module Puzzle(f) where f :: Char -> Char f c = let x = g c in h x class C a where g :: Char -> a h :: a -> Char instance C Bool where g c = c == 'T' h b = if b then 'T' else 'F' The error message from ghc is Puzzle.hs:5:12: Ambiguous type variable `a' in the top-level constraint: `C a' arising from use of `g' at Puzzle.hs:5:12 I know the technical reason why this is happening. But it's hard for me to motivate why this is reasonable. The type variable `a' is not ambiguous at all, the only type it can possibly have is Bool; any other type is an error. Furthermore, there can never be any other instance of the class C added to any program using the module Puzzle since the class C is not exported. So in what sense is this really ambiguous? I think it would be quite reasonable to allow the Puzzle module to compile, resolving `a' to be Bool. I.e., if there is only one instance that can satisfy a constraint and there is no possibility of adding instances outside the compiled module, I think resolving the overloading makes sense. -- Lennart

8 20

Low-level notation for type classes WAS: [Haskell] A puzzle and an annoying feature
by Martin Sulzmann 26 Nov '04

26 Nov '04

Hi, Daan said: > > Personally, I feel that this problem might be better solved by > making a lot of the implicit assumptions (and semantics) of type > classes more explicit, and bring them under user control. Of course, > I do have not have any idea of how this should be done concretely ;-) > > (although type class directives might be a step in the right direction?) > Well, you might not need to look that far :) To a great extent you can use Constraint Handling Rules (CHRs) to explain type classes. E.g., consider Gregory J. Duck, Simon Peyton-Jones, Peter J. Stuckey and Martin Sulzmann "Sound and Decidable Type Inference for Functional Dependencies" Peter J. Stuckey and Martin Sulzmann "A Theory of Overloading" I've just skimmed through the "Type Class Directives" paper. Pl correct me if I'm wrong but it appears that the disjoint directive can be modeled by CHRs. Example: disjoint (Integral, Fractional) can be encoded by rule Integral a, Fractional a ==> False (1) The never directive is in fact a special instance of disjoint. E.g., never Num Bool can be encoded by rule Num Bool ==> False (2) Note that the Chameleon type debugger provides type error explanation support if the error is due to rule applications such as (1) and (2). Martin

1 0

Re: [Haskell] Real life examples
by George Russell 26 Nov '04

26 Nov '04

John Meacham wrote (snipped): > I should say that efficiency is the only thing I have been concerned > about in this conversation. Well, I think my proposal can be made efficient if you try, using hash tables. There is a reason why I think top-level <- is inefficient, because it imposes a single scope for variables on the program; variables really are global. Imagine a very highly parallel program running on lots of processors, then it will be important to make sure you do not have all the processors having to constantly refer to the same global variable. Really what you need is finer control over what copies of a variable each processor uses, which is one reason why I think the extra indirection introduced by my proposal is a good idea. Consider for example Data.Unique. If you are generating lots of unique identifiers in a very highly parallel system it might well be much better for each processor to generate its own and then add a processor identifier than to have to have a central dispatcher which has to be consulted each time.

1 0

Re: Top-level <-
by George Russell 26 Nov '04

26 Nov '04

John Meacham wrote (snipped): > recursive top level declarations are no more tricky than are normal > recursive lets. Perhaps I am missing something, but surely one very important problem with <- at top level is that calling for the value of something defined by <- causes the corresponding action to be performed? Unless the actions available are very tightly restricted, this means that for example the meaning of a program depends on what order arguments to a pure functions are evaluated, for example.

1 0

Re: [Haskell] Real life examples
by George Russell 25 Nov '04

25 Nov '04

John Meacham wrote (snipped): > George Russell's library is precicly an invalid use of unsafePerformIO. > Internally, it does the invalid unsafePerformIO (newIORef) trick which > is exactly the problem we are trying to solve. hiding it in a module doesn't > make it go away. Why does it matter to you if it uses unsafePerformIO, so long as you are protected from all the unsafe consequences? Would you be happier if I required all values to instance (Read,Show) and then implemented exactly the same interface with this additional restriction using completely standard Haskell 98 by writing values to files and reading them back again? > I am not positive, but it also would also add the overhead of a > finitemap lookup across all global variables for every look up. which > doesn't really meet efficiency requirements. a global counter should > only need a single peek poke to a constant location, not some data > structure lookup. Oh really, we're not arguing about efficiency at this stage of the game are we? Actually you could implement the whole thing with a single hash table. I would have done, if TypeRep and ThreadId exposed their internal integer contents for hashing purposes.

3 2

ICTCS'05 Preliminary call for papers
by g. michele pinna 25 Nov '04

25 Nov '04

Apologies if you receive multiple copies of this mail Ninth Italian Conference on Theoretical Computer Science (ICTCS'05) Certosa di Pontignano (Siena), Italy October 12 - 14, 2005 Preliminary Call for Papers The Ninth Italian Conference on Theoretical Computer Science will take place at the Certosa di Pontignano (Siena), Italy. Papers presenting original contributions in any area of theoretical computer science are being sought. Topics include (but are not limited to): analysis and design of algorithms, computability, computational complexity, cryptography, formal languages and automata, foundations of programming languages and program analysis, foundations of artificial intelligence and knowledge representation, foundations of web programming natural computing paradigms (quantum computing, bioinformatics), parallel and distributed computation, program specification and verification, term rewriting, theory of concurrency, theory of data bases, theory of logical design and layout, type theory, security, symbolic and algebraic computation, Program Committee: Michele Bugliesi (Venezia), Mario Coppo (Torino, Co-Chair), Pierluigi Crescenzi (Firenze), Giulia Galbiati (Pavia) Luisa Gargano (Salerno), Giorgio Ghelli (Pisa), Roberto Grossi (Pisa), Benedetto Intrigila (L'Aquila), Nicola Leone (Cosenza), Elena Lodi (Siena, Co-Chair), Flaminia Luccio (Trieste), Andrea Masini (Verona), Giancarlo Mauri (Milano), Corrado Priami (Trento), Geppino Pucci (Padova), Davide Sangiorgi (Bologna). Organizing Committee: S. Brunetti (Siena), G. Michele Pinna (Cagliari - Siena, Chair), E.B.P. Tiezzi (Siena). Invited Speakers: Three invited speakers are foreseen. Names have to be announced. Dates and Deadlines: Submission Deadline: 15 April 2005 Acceptance Notification: 7 June 2005 Camera-ready deadline: 2 July 2005 Early registration deadline: 16 September 2005 Conference: 12-14 October 2005 Submissions: Authors are invited to submit electronically one copy of their extended abstract, not exceeding twelve pages. The extended abstract should clearly indicate the results achieved, their significance, and their relation to other work in the area. It is planned to publish the proceedings in the Springer Lecture Notes in Computer Science series. It is recommended to use Latex and the Springer LNCS style www.springer.de/comp/lncs. The web-based submission form will be announced soon. Conference Page: This preliminary Call For Papers is available online at the conference web page ictcs05.dsmi.unisi.it Registration Details: The registration form will be reachable from the conference web page. A limited number of grants for students and young researchers covering the registration fees are available. Details for the applications are in the conference web page.

1 0

Lexically scoped type variables
by Simon Peyton-Jones 25 Nov '04

25 Nov '04

| This is a great example, thanks for posting it. However, I feel like | the real problem in this example is the lexically-scoped type | variables declared with your function f. Paul's message gives me an excuse to consult the Haskell list about the design of lexically scoped type variables. I have a two particular questions I'd like your advice about. (This is nothing to do with monomorphism restriction, or Lennart's original puzzle.) I'm sending this message to the main Haskell list, to maximise readership, but I suggest that you reply to haskell-cafe(a)haskell.org Thereby to avoid spamming the main Haskell list, which is meant to be low-bandwidth. I believe I've set the reply-to field of this message to achieve this goal. [Perhaps others can do the same?!] Simon ---- Background ---- First, for background you might want to glance at "Lexically scoped type variables", an unpublished paper available at http://research.microsoft.com/%7Esimonpj/papers/scoped-tyvars I don't want to take time in this message to discuss why we want scoped type variables; I'll just take it for granted here. One design choice discussed in the paper, and implemented in GHC, is that we can bring new lexically-scoped type variables into scope by mentioning them in a pattern type signature: f (x::a) = .... Here 'a' is a name for the type of x, and 'a' scopes over f's body, and can be mentioned in type signatures in f's body. Sometimes one wants to name types in the result* of f, rather than it its *arguments*. For example head (xs::[a]) :: a = ... Here, the ":: a" before the "=" gives the type of head's result. If a result type signature binds a type variable, that type variable scopes over the right hand side of the definition. In GHC, it's not necessary for the type that 'a' names to be a type variable; it could be Int, for example: f (x::a) = x + (1::Int) Already this embodies several design choices. For example, we know that 'a' is a *binding* for 'a' because there is no 'a' already in scope, otherwise it'd be an *occurrence* of 'a'. (An alternative would be to mark binding sites somehow.) Also once could require that 'a' names a type variable rather than an arbitrary type. But for this message I want to take GHC's design as given. ---- QUESTION 1 ----- In GHC at present, a separate type signature introduces no scoping. For example: f :: forall a. a -> a f x = (x::a) would be rejected, because the type signature for 'f' does not make anything scope over the right-hand side, so (x::a) means (x::forall a.a), which is ill typed. An obvious alternative, taken up by (among others) Mondrian and Chamaeleon, is to say that the top-level quantified variables of a separate type signature scope over the right hand side of the binding In the above example, then, the 'a' bound by the 'forall' would scope over the right hand side of 'f'. I've argued against this in the past, because the construct (forall a. <type>) patently scopes 'a' only over <type>. But my resolve is weakening. It's just too convenient! Furthermore, it binds a *rigid* type variable (i.e. 'a' really must name a type variable) and that's important for GADTs... which strengthens the case. In short, I'm considering adopting the Mondrian/Chameleon rule for GHC. There are two variations 1a) In the example, 'a' is only brought into scope in the right hand side if there's an explicit 'forall' written by the programmer 1b) It's brought into scope even if the forall is implicit; e.g. f :: a -> a f x = (x::a) I'm inclined to (1a). Coments? ----- QUESTION 2 ------ Question 2 concerns degenerate bindings. First, consider pattern bindings. For example: let (x::[a], y) = <rhs> in <body> The LHS of the let-binding is a pair, so it's called a pattern binding. What should the scope of 'a' be? GHC's current story is that "it is the same as the scope of term variables bound in the same pattern", so just as 'x' scopes over both <rhs> and <body>, so does 'a'. And that in turn means that we can't generalise over 'a', so 'x' is monomorphic. An alternative would be to say that type variables bound in a pattern binding scope only over the right-hand side. ---- The degenerate case: variable bindings ---- Now the nasty case let f :: a -> a = \x -> x in (f True, f 'c') Is the binding for 'f' (A) a (degenerate) function binding no arguments, but with a result signature? or (B) a (degenerate) pattern binding with pattern (var::type)? If we consider it to be (A) then arguably 'a' scopes only over the right-hand side, and f gets the polymorphic type (forall a. a-> a). If we consider it to be (B) then currently 'a' scopes over the right hand side and the body of the let, so 'f' has to be monomorphic, with type ty->ty for some ty; and no ty will do, so the program is rejected. The trouble is that the binding is patently *both* (A) and (B). This gives no difficulty in Haskell 98, because there's no difference in treatment; but GHC's current rules for scoped type variables do distinguish the two. The alternatives I can see are 2a) Make an arbitrary choice of (A) or (B); GHC currently chooses (B) 2b) Decide that the scoped type variables arising from pattern bindings scope only over the right hand side, not over the body of the let 2b) Get rid of result type signatures altogether; instead, use choice (1a) or (1b), and use a separate type signature instead. Opinions?

1 0

Top-level <-
by George Russell 25 Nov '04

25 Nov '04

John Meacham wrote: > Now, my mdo proposal as written would have "hello" outputed exactly once > at module start up time no matter what, whether x is demanded or not. it > is equivalant to a program transformation that collects all the top > level initializers and declarations, puts them all in a mdo block and > runs it with the semantics explained in the fixIO paper. (with a > deterministic, but partially undefined order) What happens if you write the following? y <- f x <- .... let f = something depending on x Will it know to evaluate x before y, or is this not allowed? What about if the assignments to y and x occur in different modules? Will the RTS have to analyse the dependencies to work out which order to run the assignments in?`

2 1