big lambda in class declarations

[Hal Daume III]

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
>