Skip to Main content Skip to Navigation

MLF: An extension of ML with first-class polymorphism and implicit instantiation

Abstract : We propose a type system MLF that generalizes ML with first-class
polymorphism as in System F. Expressions may contain second-order type
annotations. Every typable expression admits a principal type, which
however depends on type annotations. Principal types capture all other
types that can be obtained by implicit type instantiation
and they can be inferred.

All expressions of ML are well-typed without any annotations.
All expressions of System F can be mechanically encoded into MLF
by dropping all type abstractions and type applications,
and injecting type annotations of lambda-abstractions into MLF types.
Moreover, only parameters of lambda-abstractions that are used
polymorphically need to remain annotated.
Document type :
Complete list of metadata

Cited literature [83 references]  Display  Hide  Download
Contributor : Didier Le Botlan Connect in order to contact the contributor
Submitted on : Friday, October 15, 2004 - 3:50:51 PM
Last modification on : Friday, February 4, 2022 - 3:10:32 AM
Long-term archiving on: : Friday, April 2, 2010 - 8:33:15 PM


  • HAL Id : tel-00007132, version 1



Didier Le Botlan. MLF: An extension of ML with first-class polymorphism and implicit instantiation. Other [cs.OH]. Ecole Polytechnique X, 2004. English. ⟨tel-00007132⟩



Record views


Files downloads