2009, English, Article edition: Recasting MLF Le Botlan, Didier; Rémy, Didier

User activity

Share to:
 
Bookmark: http://trove.nla.gov.au/version/204100
Physical Description
  • text
Published
  • HAL - CCSD
  • 2009
Language
  • English

Edition details

Title
  • Recasting MLF
Author
  • Le Botlan, Didier
  • Rémy, Didier
Published
  • HAL - CCSD
  • 2009
Physical Description
  • text
Subjects
Notes
  • 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.
  • HAL:inria-00156628, version 4
  • HAL:http:/​/​hal.inria.fr/​inria-00156628/​en/​
  • DOI:10.1016/​j.ic.2008.12.006
Language
  • English
Contributed by
OAIster

Get this edition

  • Set up My libraries

    How do I set up "My libraries"?

    In order to set up a list of libraries that you have access to, you must first login or sign up. Then set up a personal list of libraries from your profile page by clicking on your user name at the top right of any screen.

  • All (1)
  • Unknown (1)
None of your libraries hold this item.
None of your libraries hold this item.
None of your libraries hold this item.
None of your libraries hold this item.
None of your libraries hold this item.
None of your libraries hold this item.
None of your libraries hold this item.
None of your libraries hold this item.

User activity


e.g. test cricket, Perth (WA), "Parkes, Henry"

Separate different tags with a comma. To include a comma in your tag, surround the tag with double quotes.

Be the first to add a tag for this edition

Be the first to add this to a list

Comments and reviews

What are comments? Add a comment

No user comments or reviews for this version

Add a comment