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 i ML F of ML F and provide an interpretation of i ML F types as instantiation-closed sets of Dash System-F types, from which we derive the definition of type-instance in i ML F. We give equivalent syntactic definition of the type-instance, presented as a set of inference rules. We also show an encoding of i ML F into the closure of Curry-style System F by let-expansion. We derive the Church-style version e ML F by refining types of i ML F so as to distinguish between given and inferred polymorphism. We show an embedding of ML in e ML F and a straightforward encoding of System F into e ML F.

Authors

• Didier Le Botlan
• Didier Rémy

Keywords

• ML
• System F
• Type inference
• Type checking
• Polymorphism
• First-class polymorphism