Recasting MLF

Abstract : The language MLF has been proposed as an alternative to System F that permits partial type inference a la ML. It differs from System F by its types and type-instance relation. Unfortunately, the definition of type instance is only syntactic, and not underpined by some underlying semantics. It has so far only been justified a posteriori by the type soundness result. In this work, we revisit MLF following a more progressive approach stepping on System F. We argue that System F is not a well-suited language for ML-style type inference because it fails to factorize some closely related typing derivations. We solve this problem in Curry's style MLF by enriching types with a new form of quantification that may represent a whole collection of System F types. This permits a natural interpretation of MLF types as sets of System-F types and pulling back the instance relation from set inclusion on the interpretations. We also give an equivalent syntactic definition of the type-instance, presented as a set of inference rules. We derive a Church's style version of MLF by further refining types so as to distinguish between user-provided and inferred type information. The resulting language is more canonical than the one originally proposed. We show an embedding of ML in MLF and an encoding of System F into MLF. Besides, as MLF is more expressive than System F, an encoding of MLF is given towards an extension of System F with local binders.
Type de document :
[Research Report] RR-6228, 2007, pp.60
Liste complète des métadonnées
Contributeur : Didier Rémy <>
Soumis le : mardi 10 juillet 2007 - 14:56:40
Dernière modification le : mardi 11 septembre 2018 - 15:18:15
Document(s) archivé(s) le : jeudi 23 septembre 2010 - 16:00:40


Fichiers produits par l'(les) auteur(s)


  • HAL Id : inria-00156628, version 3



Didier Le Botlan, Didier Rémy. Recasting MLF. [Research Report] RR-6228, 2007, pp.60. 〈inria-00156628v3〉



Consultations de la notice


Téléchargements de fichiers