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