It seems that the inability to have (\x . x) as a type in the Theimann et al approach is a severe limitation. I don't think that having to help the typechecker along, as in boundless rank polymorphism, is a bad thing at all.
-- Hal Daume III | [EMAIL PROTECTED] "Arrest this man, he talks in maths." | www.isi.edu/~hdaume On Wed, 5 Mar 2003, Simon Peyton-Jones wrote: > Big lambda is in terms. You mean a "lambda at the type level", which is > usually written as a small lambda. Confusing, I know. > > There's an ICFP02 paper on the subject, by Thiemann et al. Worth a > read. > > Problem with inference is that the type checker can't guess lambdas. > Suppose we need to unify > > m Int > with > ST Int Int > > One possibility is > > m = ST > > Another is > > m = \t. ST t Int > > Another is > > m = \t. ST Int t > > > One solution is to restrict what lambdas are allowable, and that is what > Thiemann et al do. Another is to declare the typechecker should never > guess a lambda; instead the programmer has to specify what lambda to use > whenever there is doubt. That is the approach that we're ruminating on > here. Stay tuned, but don't hold your breath. > > Simon > > | -----Original Message----- > | From: Hal Daume III [mailto:[EMAIL PROTECTED] > | Sent: 04 March 2003 16:34 > | To: Haskell Mailing List > | Subject: big lambda in class declarations > | > | So the word on the street is that allowing big lambda makes type > inference > | undecidable. This makes sense to me since allowing big lambda > essentially > | allows you to program at the type level and thus of course you'll get > | undecidability. > | > | However, I'm having difficulty understanding where the undecidability > | sneaks in if you allow big lambda in class declarations. I suppose > the > | cannonical example is when you want to write something like: > | > | > class Set s where { ... } > | > instance Set (/\ a. FiniteMap a ()) where { ... } > | > | but now you have to write: > | > | > data FMSet a = FMSet (FiniteMap a ()) > | > instance Set FMSet where { ... } > | > | The big lambda is of course equivalent to not applying type synonyms > | completely, somethign like: > | > | > type FM a = FiniteMap a () > | > instance Set FM where { ... } > | > | will of course also be rejected (since this would give us a way to do > big > | lambda). > | > | Could some one help my intuition a bit here and explain to me how you > | could use big lambdas in class declarations to write programs? > | > | Thanks! > | > | - Hal > | > | -- > | Hal Daume III | [EMAIL PROTECTED] > | "Arrest this man, he talks in maths." | www.isi.edu/~hdaume > | > | _______________________________________________ > | Haskell mailing list > | [EMAIL PROTECTED] > | http://www.haskell.org/mailman/listinfo/haskell > _______________________________________________ Haskell mailing list [EMAIL PROTECTED] http://www.haskell.org/mailman/listinfo/haskell
