s'authentifier
version française rss feed

inria-00156628, version 4

Recasting MLF

Didier Le Botlan () 1, Didier 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.

 
  • inria-00156628, version 4
  • oai:hal.inria.fr:inria-00156628
  • Contributeur : 
  • Soumis le : Mercredi 3 Décembre 2008, 14:02:23
  • Dernière modification le : Mardi 28 Juillet 2009, 15:43:09
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...