[TYPES] System F and implicit instantiation

[Thorsten Altenkirch]

Jeremy Graham Siek wrote:

>[The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list]
>
>Hi All,
>
>Type checking for System F with church-style terms is easy. How difficult
>does type checking become if instantiation is made implicit?
>  
>
It is undecidable, because you can reduce 2nd order unification to it. 
Frank Pfenning
showed this quite a while ago (actually 92), long before Joe Wells 
showed that the Curry System
is undecidable. In my opinion is the Pfenning result more relevant for 
showing that
type inference for System F is undecidable.

See
http://www.cs.cmu.edu/~fp/papers/CMU-CS-92-105.pdf

Cheers,
Thorsten

This message has been scanned but we cannot guarantee that it and any
attachments are free from viruses or other damaging content: you are
advised to perform your own checks.  Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.