OK. I've been doing a little thinking about type lambda in Haskell.
Now, I understand the prevailing wisdom is that adding type lambda
and/or partially applied type synonyms to the haskell type system
would make type checking/inference undecidable. The reason given is
that higher-order unification is undecidable.
I have to admit that I don't fully understand this reason. Setting
aside typeclasses for now, it seems to me that type expressions
together with the kind system are just the simply-typed lambda
calculus with unit, which is well known to be strong normalizing. So
any type with kind * has a normal form with (by definition) no
internal redexes. I think this is sufficient to guarantee that all
type lambdas are removed. Now you can proceed using first-order
unification, which is decidable. Of course, all valid expressions
have kind * (ignoring unboxing and other trickiness for now).
So where have I gone wrong? Do typeclasses complicate the matter?
Or have I missed something more basic?
Thanks,
Rob Dockins
Speak softly and drive a Sherman tank.
Laugh hard; it's a long way to the bank.
-- TMBG
_______________________________________________
Haskell-Cafe mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell-cafe
