Recasting MLF

The language ML^F is a proposal for a new type system that supersedes both ML and System F, allows for efficient, predictable, and complete type inference for partially annotated terms. In this work, we revisit the definition of ML^F, following a more progressive approach and focusing on the design-space and expressiveness. We introduce a Curry-style version iML^F of ML^F and provide an interpretation of iML^F types as instantiation-closed sets of Dash System-F types, from which we derive the definition of type-instance in iML^F. We give equivalent syntactic definition of the type-instance, presented as a set of inference rules. We also show an encoding of iML^F into the closure of Curry-style System F by let-expansion. We derive the Church-style version eML^F by refining types of iML^F so as to distinguish between given and inferred polymorphism. We show an embedding of ML in eML^F and a straightforward encoding of System F into eML^F.