[Haskell-cafe] question about type lambda and decidability of
robdockins at fastmail.fm
Fri Feb 10 18:19:27 EST 2006
For the record, a little more digging turned up this
which answers most of my questions.
On Feb 10, 2006, at 2:02 PM, Robert Dockins wrote:
> 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?
> Rob Dockins
> Speak softly and drive a Sherman tank.
> Laugh hard; it's a long way to the bank.
> -- TMBG
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
Speak softly and drive a Sherman tank.
Laugh hard; it's a long way to the bank.
More information about the Haskell-Cafe