big lambda in class declarations

[Simon Peyton-Jones]

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 =3D ST

Another is
=09
	m =3D \t. ST t Int

Another is

	m =3D \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
|=20
| 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.
|=20
| 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:
|=20
| > class Set s where { ... }
| > instance Set (/\ a. FiniteMap a ()) where { ... }
|=20
| but now you have to write:
|=20
| > data FMSet a =3D FMSet (FiniteMap a ())
| > instance Set FMSet where { ... }
|=20
| The big lambda is of course equivalent to not applying type synonyms
| completely, somethign like:
|=20
| > type FM a =3D FiniteMap a ()
| > instance Set FM where { ... }
|=20
| will of course also be rejected (since this would give us a way to do
big
| lambda).
|=20
| 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?
|=20
| Thanks!
|=20
|  - Hal
|=20
| --
|  Hal Daume III                                   | hdaume@isi.edu
|  "Arrest this man, he talks in maths."           | www.isi.edu/~hdaume
|=20
| _______________________________________________
| Haskell mailing list
| Haskell@haskell.org
| http://www.haskell.org/mailman/listinfo/haskell