inria-00156628, version 4
Recasting MLF
Didier Le Botlan
1Didier Rémy
2
Information and Computation 207, 6 (2009) 726-785
Résumé : 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.
- 1 : Laboratoire d'analyse et d'architecture des systèmes (LAAS)
- CNRS : UPR8001 – Université Paul Sabatier - Toulouse III – Institut National Polytechnique de Toulouse - INPT – Institut National des Sciences Appliquées de Toulouse
- 2 : GALLIUM (INRIA Rocquencourt)
- INRIA
- Domaine : Informatique/Langage de programmation
- Mots-clés : System-F MLF Unification Types Graphs Binders Inference
- Référence interne : RR-6228
- Versions disponibles : v1 (22-06-2007) v2 (25-06-2007) v3 (10-07-2007) v4 (03-12-2008)
- inria-00156628, version 4
- http://hal.inria.fr/inria-00156628
- oai:hal.inria.fr:inria-00156628
- Contributeur : Didier Rémy
- Soumis le : Mercredi 3 Décembre 2008, 14:02:23
- Dernière modification le : Mardi 28 Juillet 2009, 15:43:09






Documents associés
Exporter