[TYPES] System F and implicit instantiation

[Jeremy Siek]

Hi Thorsten,

The problem of partial type reconstruction considered by Frank Pfenning
in the paper you refer to is a bit different than what I'm interested 
in.
It allows for the erasure of type annotations on lambda bound 
parameters,
and requires markers to be left where type application occurs. I'm 
interested
in what happens when type annotations are required on lambda bound 
parameters
but type application is inferred. I don't know whether his results 
carry over
to this situation.

Cheers,
Jeremy

On Aug 9, 2004, at 8:55 AM, Thorsten Altenkirch wrote:

> 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.
>
_______________________________________________
Jeremy Siek <jsiek at osl.iu.edu>
http://www.osl.iu.edu/~jsiek
Ph.D. Student, Indiana University Bloomington
C++ Booster (http://www.boost.org)
_______________________________________________