April 2002 - Haskell - Haskell.org

CALL FOR PROPOSALS FOR ORGANIZING ICLP'03
by Dr. Gopal Gupta 05 Apr '02

05 Apr '02

CALL FOR PROPOSALS FOR ORGANIZING ICLP'03 The Association for Logic Programming (ALP) invites proposals for organizing the 19th International Conference on Logic Programming (ICLP) in the year 2003. The ICLP is ALP's and the logic programming communities' flagship conference where most recent advancements in logic programming are presented. The conference is attended by researchers interested in logic programming, constraint programming, programming languages, AI and other affiliated fields. The last few ICLPs were held in: Copenhagen (2002), Paphos/Cyprus (2001), London (2000), Las Cruces/NM (1999). If you are interested in organizing ICLP'03, please get in touch with me asap. More details of what is entailed in proposing to organize an ICLP can be found in ALP's website: http://www.cwi.nl/projects/alp/ (click on "ALP policy" button at the bottom of the index bar). Gopal Gupta (gupta(a)utdallas.edu) ALP Conference Coordinator (Apologies for multiple messages.)

1 0

explicitly quantified classes in functions
by Hal Daume III 05 Apr '02

05 Apr '02

Why can I not define the following (in ghc): > class Foo p where > instance Foo Double where > foo :: Double -> (forall q . Foo q => q) > foo p = p >From my humble (lack of) knowledge, there seems to be nothing wrong here, but ghc (5.03) complains about unifying q with Double. I *can* write: > class Foo p where > instance Foo Double where > data T = forall q . Foo q => T q > foo :: Double -> T > foo p = T p which is very similar, except that the explicit universal quantification is happening in in the datatype and not the function type. why is the former disallowed? -- Hal Daume III "Computer science is no more about computers | hdaume(a)isi.edu than astronomy is about telescopes." -Dijkstra | www.isi.edu/~hdaume

2 1

Re: explicitly quantified classes in functions
by John Hughes 04 Apr '02

04 Apr '02

Why can I not define the following (in ghc): > class Foo p where > instance Foo Double where > foo :: Double -> (forall q . Foo q => q) > foo p = p From my humble (lack of) knowledge, there seems to be nothing wrong here, but ghc (5.03) complains about unifying q with Double. Well, of course! The result has to have type (forall q . Foo q => q), but p actually has type Double. Of course GHC complains. The question is, why YOU think it is OK. And the answer is that you reason: there is only one instance of Foo, so when I say Foo q, that means q must be Double. But you're making the "closed world assumption", that you know all of the instances of Foo. The compiler doesn't, and for good reason. Suppose you were to export these definitions from the module where they appear, into another module which defines instance Foo Integer Now, of course, it should be OK to use Foo with the type Double -> Integer (since Foo Integer holds in this context). Yet clearly, the *definition* you gave cannot be used with this type. Hence the type is wrong. Of course, you could argue that if the definition of foo is *not* exported, then the compiler should use the closed world assumption and the program should be accepted. But it would be really weird if whether a definition is well-typed or not depended on whether or not it was exported... John

2 1

Double -> non-double function :)
by Hal Daume III 04 Apr '02

04 Apr '02

I'm looking for a (not-necessarily Haskell 98 compliant, as long as it works in GHC) way to get at the internal representation of Doubles. I can use decodeDouble# to get at it, but I need something equivalent to encodeDouble# to go the other way, and I cannot find such a function anywhere. Any suggestions are welcome (yes, I know I can use show and read, but I'm looking for something which will keep the # of bytes down). - Hal -- Hal Daume III "Computer science is no more about computers | hdaume(a)isi.edu than astronomy is about telescopes." -Dijkstra | www.isi.edu/~hdaume

3 3

RE: deriving over renamed types
by Simon Peyton-Jones 04 Apr '02

04 Apr '02

| > ...which would be very useful, but would probably have unpleasant | > consequences for type inference... | | To my mind, this is not a credible objection. The horse has | already bolted; there's no point in trying to shut the stable | door. The existing post-Hindley-Milner aspects of Haskell's | type system are too useful for type inference to be worthy of | such veneration. I agree with this. The goal of 100% type inference is a red herring. This point of view is articulated at some length in a draft paper Mark Shields and I have written, on scoped type variables http://research.microsoft.com/~simonpj/papers/scoped-tyvars Type inference is still terrifically useful to "fill in the gaps" between programmer-supplied type signatures. The trouble with full type lambdas is that they make unification essentially impossible, and that has a huge impact on how many type annotations you need. So I'm completely in agreement with moving towards allowing the programmer to supply more explicit type information; but I have not yet seen a proposal that supports anything like full type lambdas in a system that looks anything like an extension of Haskell, and that does not require quite burdensome type annotations. But I may well simply be ignorant. Simon

1 0

Re: deriving over renamed types
by Ashley Yakeley 04 Apr '02

04 Apr '02

At 2002-04-03 15:14, Hal Daume III wrote: >if I replace > >> type FM = FiniteMap > >with > >> type FM a b = FiniteMap a b > >it works fine. I wasn't aware there was (supposed to be) a difference >between these two declarations? Is there? I don't know about your example, but there is a difference. type FM = FiniteMap ...This defines FM as a type-constructor of kind (* -> * -> *) equivalent to FiniteMap. type FM a b = FiniteMap a b ...This defines FM as a pseudo-type-constructor. It has no kind, but must be specified with two arguments each of kind (*) so as to become a type-constructor (a type) of kind (*). Unfortunately Haskell does not have lambda over types, otherwise the two could be the same. And then one could do things such as type M b a = a -> b; instance Cofunctor (M b) where ... ...which would be very useful, but would probably have unpleasant consequences for type inference... -- Ashley Yakeley, Seattle WA

2 1

Final cfp: WRS'02 - 2nd WS on Reduction Strategies, deadline: April 15
by Bernhard Gramlich 04 Apr '02

04 Apr '02

[Apologies for multiple copies of this announcement] ************************************************************************** **************** final call for papers and participation *************** ************************************************************************** Second International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2002) http://www.dsic.upv.es/users/elp/WRS2002 affiliated with RTA 2002, held as part of FLoC 2002 Copenhagen, Denmark, July 21, 2002 -------------------------------------------------------------------------- BACKGROUND AND AIMS Reduction strategies in rewriting and programming have attracted an increasing attention within the last years. New types of reduction strategies have been invented and investigated, and new results on rewriting / computation under particular strategies have been obtained. Research in this field ranges from primarily theoretical questions about reduction strategies to very practical application and implementation issues. The need for a deeper understanding of reduction strategies in rewriting and programming, both in theory and practice, is obvious, since they bridge the gap between unrestricted general rewriting (computation) and (more deterministic) rewriting with particular strategies (programming). Moreover, reduction strategies provide a natural way to go from operational principles (e.g., graph and term rewriting, narrowing, lambda-calculus) and semantics (e.g., normalization, computation of values, infinitary normalization, head-normalization) to implementations of programming languages. Therefore any progress in this area is likely to be of interest not only to the rewriting community, but also to neighbouring fields like functional programming, functional-logic programming, and termination proofs of algorithms. The workshop wants to provide a forum for the presentation and discussion of new ideas and results, recent developments, new research directions, as well as of surveys on existing knowledge in this area. Furthermore we aim at fostering interaction and exchange between researchers and students actively working on such topics. The workshop will be held in conjunction with RTA 2002 in Copenhagen (Denmark) on July 21, 2002. The workshop is (co-)organized by TU Valencia and TU Wien. TOPICS OF INTEREST Topics of interest include, but are not restricted to: - theoretical foundations for the definition and semantic description of reduction strategies - strategies in different frameworks (term rewriting, graph rewriting, infinitary rewriting, lambda calculi, higher order rewriting and explicit substitutions, conditional rewriting, rewriting with built-ins, narrowing, constraint solving, etc.) and their application in (equational, functional, functional-logic) programming (languages) - properties of reduction strategies / computations under strategies (e.g., completeness, computability, decidability, complexity, optimality, (hyper-)normalization, cofinality, fairness, perpetuality, context-freeness, neededness, laziness, eagerness, strictness) - interrelations, combinations and applications of reduction under different strategies (e.g., equivalence conditions for fundamental properties like termination and confluence, applications in modularity analysis, connections between strategies of different frameworks, etc.) - program analysis and other semantics-based optimization techniques dealing with reduction strategies - rewrite systems / tools / implementations with flexible / programmable strategies as essential concept / ingredient - specification of reduction strategies in (real) languages - data structures and implementation techniques for reduction strategies. SUBMISSIONS We solicit papers on all aspects of reduction strategies in rewriting and programming. Submissions should describe unpublished work, except for survey papers which are explicitly welcome, too. Submissions should not exceed 10 pages (however, survey papers may be longer) and be sent in postscript format to the PC co-chairs at wrs02(a)dsic.upv.es before April 15, 2002. Submissions should include the title, authors' names, affiliations, addresses, and e-mail. Selection of papers by the PC will be based on originality, significance, and correctness. Final versions will be due by June 17, 2002. PUBLICATION The final workshop proceedings will be published in the Electronic Notes in Theoretical Computer Science (ENTCS) series of Elsevier. Preliminary hardcopy proceedings will be available at the workshop. A special issue of the Journal of Symbolic Computation (JSC) on Reduction Strategies in Rewriting and Programming will be designated for revised and extended versions of selected contributions from both WRS 2001 (Utrecht, May 2001) and WRS 2002. PROGRAM COMMITTEE Sergio Antoy Portland (USA) Roberto Di Cosmo Paris VII (France) Bernhard Gramlich (co-chair) Wien (Austria) Michael Hanus Kiel (Germany) Claude Kirchner Nancy (France) Paul Klint CWI Amsterdam (The Netherlands) Salvador Lucas (co-chair) Valencia (Spain) Manfred Schmidt-Schauss Frankfurt am Main (Germany) Yoshihito Toyama Tohoku (Japan) ORGANIZERS Bernhard Gramlich (co-chair) Technische Universitaet Wien Salvador Lucas (co-chair) Universidad Politecnica de Valencia INVITED TALKS (with tentative titles) Aart Middeldorp, Tsukuba (Japan): Strategies for Term Rewriting Vincent van Oostrom, Utrecht (The Netherlands): Optimal Strategies in Higher-Order Rewriting IMPORTANT DATES Deadline for submissions: April 15, 2002 Notification: May 27, 2002 Final versions due: June 17, 2002 Workshop: July 21, 2002 FURTHER INFORMATION WRS 2002 website: http://www.dsic.upv.es/users/elp/WRS2002 WRS 2002 e-mail address: wrs02(a)dsic.upv.es RTA 2002 website: http://www.ericsson.com/cslab/rta2002/ FLoC 2002 website: http://floc02.diku.dk WRS 2002 website at FLoC: http://floc02.diku.dk/WRS **************************************************************************

1 0

deriving over renamed types
by Hal Daume III 04 Apr '02

04 Apr '02

Why can't I do this: > import FiniteMap > type FM = FiniteMap > instance (Show a, Show b) => Show (FiniteMap a b) where > show = show . fmToList > data X = X (FM Int Int) > deriving (Show) if I replace > type FM = FiniteMap with > type FM a b = FiniteMap a b it works fine. I wasn't aware there was (supposed to be) a difference between these two declarations? Is there? - Hal -- Hal Daume III "Computer science is no more about computers | hdaume(a)isi.edu than astronomy is about telescopes." -Dijkstra | www.isi.edu/~hdaume

1 0

RE: ">>" and "do" notation
by Simon Peyton-Jones 03 Apr '02

03 Apr '02

| > I think the point that's being missed in this discussion | > is that a monad is a n *abstract* type, and sometimes the | > natural "equality" on the abstract type is not the same as | > equality on representations. ... If we can give >> a | more efficient | > implementation, which constructs a better representation | > than >>= does, that's fine, as long as the two | > representations "mean" the same thing. | | Point taken, but I remain unconvinced. What comes out of the | monad /isn't/ abstract; there's nothing to ensure that | subsequent use respects the abstraction. | | That's true, of course. But *should* we insist that the | programming language guarantee that abstractions are always | respected? i.e. equivalent representations are always treated | equivalently? This is an interesting discussion but from the point of view of H98 I'm interested in answering the following much narrower question: what should be the desugaring of do { e ; Q } The current Report uses (>>) for this, and (>>=) for the "p <- e" case. An alternative would be to use (>>=) for both. I take it for granted that (>>) stays as an operation of class Monad: several people have argued for this, and I have no intention of changing H98 in that respect. I take it for granted that if the Report says "use >>" then implementations should. So either GHC and Hugs have to change or the Report does. So the question remains: what would be best for programmers: A: the predictability that desugaring do-notation uses only (>>=) and return, or B: or the extra power of using (>>) for the no-patterns case? If there are Good Reasons for having (>>) in the class, as several have argued, then I guess we should go for (B). In that case the Report would stay unchanged, and the impls would have to change. I also thought that James's analogy of (-x) translating to (negate x) and not to (0-x) was a good one. I originally favoured (A) but I'm happy to go with (B). anyone disagree? Simon

1 0

Re: ">>" and "do" notation
by John Hughes 03 Apr '02

03 Apr '02

> I think the point that's being missed in this discussion > is that a monad is a n *abstract* type, and sometimes the > natural "equality" on the abstract type is not the same as > equality on representations. ... If we can give >> a more efficient > implementation, which constructs a better representation > than >>= does, that's fine, as long as the two > representations "mean" the same thing. Point taken, but I remain unconvinced. What comes out of the monad /isn't/ abstract; there's nothing to ensure that subsequent use respects the abstraction. That's true, of course. But *should* we insist that the programming language guarantee that abstractions are always respected? i.e. equivalent representations are always treated equivalently? We don't always in other contexts. To take an example, consider a bag datatype with a bagFold operator and an Eq instance that implements bag equality. Then xBag == yBag doesn't necessarily imply bagFold op z xBag == bagFold op z yBag We rely on the programmer to use bagFold properly, i.e. supply an AC op with unit z. If he doesn't, the abstraction is broken. > This is all perfectly respectable, and has to do with the > fact that Haskell i s a programming language, not > mathematics -- so we represent equivalence classe s by > values chosen from them. For the *language* to rule out > constructing different representations for "equivalent" > constructions, such as >> and >>=, would be unreasonable. Here's the problem. Your argument sounds very similar to the one against type checking. That /you/ can get it right doesn't encourage me to believe that J Random Hacker isn't going to abuse the facility. It's not as if you couldn't define >!= and >! for something that's nearly a monad, it would just stop you using the do notation, which is, I think fair, since Haskell provides no way of selecting the correct form of equality for do {_ <- A; B} == do {A; B}. Jón This is a much bigger cost than you make out. Making something into a monad allows not only the use of the do syntax, it allows the use of a large number of generic monad operations, the application of monad transformers, etc etc. It's a big deal. I agree there's an analogy here with type-checking here. Indeed, there's a tradeoff where typechecking is concerned too: we give up some flexibility for greater safety. We accept that nowadays, because the flexibility we give up with Hindley-Milner typing is not so great, and the gain in safety is considerable. But would you argue that we should prohibit programs which potentially break an abstraction? I.e. prohibit bagFold, or alternatively allow it only for operators which the compiler can *decide* are AC? Would you want to prohibit monad instances which the compiler cannot decide satisfy the monad laws? I know you would want to prohibit monad instances where the compiler cannot decide that >> and >>= are properly related. The trouble is that prohibiting bagFold, separate definitions of >>, etc. altogether is quite a big cost: such things are very useful! Yet we lack the analogue of the Hindley-Milner type system -- a way for the compiler to *decide* that a monad instance, an ADT definition, or whatever, is OK, which is *proven* sufficiently flexible to handle almost all practical cases. In its absence, the analogy with type-checking is not compelling. If all we had was a monomorphic type system, then I would be against imposing type-checking too. Perhaps there's an interesting research direction here for somebody... John

1 0