[TYPES] System F and implicit instantiation

[Didier Remy]

Jeremy Siek <jsiek at osl.iu.edu> writes:

> 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.

Hi Jeremy,

You may have a look at MLF (http://pauillac.inria.fr/~remy/work/mlf/).  In
MLF all type abstractions and type applications are left implicit.  Type
annotations must be put on some lambda-abstractions (and may be put on
all). Types are slightly richer than those of System F (but remain second
order). You may restrict type annotations to System-F types and still reach
all of System F terms. However, the inferred types will still show you a
little more information.

Best regards,

        Didier