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 underpinned 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 building on System F. We argue that System F is not a well-suited language for ML-style type inference because it fails to share some closely related typing derivations. We solve this problem in Curry 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 defining the instance relation as set containment of the interpretations. We also give an equivalent syntactic definition of the type-instance, presented as a set of inference rules. We derive a Church-style version of MLF by further refining types so as to distinguish between user-provided and inferred type information. 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 :
Article dans une revue
Information and Computation, Elsevier, 2009, Volume 207, Issue 6, June 2009, Pages 726-785, 207 (6), pp.726-785. <10.1016/j.ic.2008.12.006>
Liste complète des métadonnées


https://hal.inria.fr/inria-00156628
Contributeur : Didier Rémy <>
Soumis le : mercredi 3 décembre 2008 - 14:02:23
Dernière modification le : mardi 10 janvier 2017 - 15:13:02
Document(s) archivé(s) le : vendredi 24 septembre 2010 - 11:16:17

Fichier

recasting-mlf-RR.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Didier Le Botlan, Didier Rémy. Recasting MLF. Information and Computation, Elsevier, 2009, Volume 207, Issue 6, June 2009, Pages 726-785, 207 (6), pp.726-785. <10.1016/j.ic.2008.12.006>. <inria-00156628v4>

Partager

Métriques

Consultations de
la notice

351

Téléchargements du document

104