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 | hdaume@isi.edu "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:hdaume@ISI.EDU] | 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 | hdaume@isi.edu | "Arrest this man, he talks in maths." | www.isi.edu/~hdaume | | _______________________________________________ | Haskell mailing list | Haskell@haskell.org | http://www.haskell.org/mailman/listinfo/haskell