MLF made simple
Résumé
We propose MLF---a type system that supersedes both ML and System F and enables complete type inference for partially annotated programs based on first-order unification and let-polymorphism. This variant of MLF is less expressive than the original one, yet it retains all its essential properties. In Curry's style, this variant uses {\Dash\SystemF} types extended with flexible bindings that can be interpreted as sets of System-F types. The type instance relation may be derived from the interpretation. We may also exhibit a translation from MLF to an extension of System F with local-bindings. In Church's style, only function parameters that are used polymorphicallyneed to be annotated as all other type annotations may be inferred.
Origine : Fichiers produits par l'(les) auteur(s)