Recasting MLF

The language MLF 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 MLF, following a more progressive approach and focusing on the design-space and expressiveness. We introduce a Curry-style version iMLF of MLF and provide an interpretation of iMLF types as instantiation-closed sets of Dash System-F types, from which we derive the definition of type-instance in iMLF. We give equivalent syntactic definition of the type-instance, presented as a set of inference rules. We also show an encoding of iMLF into the closure of Curry-style System F by let-expansion. We derive the Church-style version eMLF by refining types of iMLF so as to distinguish between given and inferred polymorphism. We show an embedding of ML in eMLF and a straightforward encoding of System F into eMLF.