question about type lambda and decidability of typechecking

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
2 messages Options
Reply | Threaded
Open this post in threaded view
|

question about type lambda and decidability of typechecking

Bugzilla from robdockins@fastmail.fm
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: question about type lambda and decidability of typechecking

Bugzilla from robdockins@fastmail.fm
For the record, a little more digging turned up this

http://portal.acm.org/citation.cfm?id=583852.581496

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?
>
>
> 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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe



Speak softly and drive a Sherman tank.
Laugh hard; it's a long way to the bank.
           -- TMBG


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe