HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Journal articles

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.
Document type :
Journal articles
Complete list of metadata

Cited literature [57 references]  Display  Hide  Download

https://hal.inria.fr/inria-00156628
Contributor : Didier Rémy Connect in order to contact the contributor
Submitted on : Wednesday, December 3, 2008 - 2:02:23 PM
Last modification on : Tuesday, April 5, 2022 - 3:43:38 AM
Long-term archiving on: : Friday, September 24, 2010 - 11:16:17 AM

File

recasting-mlf-RR.pdf
Files produced by the author(s)

Identifiers

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⟩

Share

Metrics

Record views

367

Files downloads

481