Skip to Main content Skip to Navigation
Theses

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 :
Theses
Complete list of metadatas

Cited literature [83 references]  Display  Hide  Download

https://pastel.archives-ouvertes.fr/tel-00007132
Contributor : Didier Le Botlan <>
Submitted on : Friday, October 15, 2004 - 3:50:51 PM
Last modification on : Thursday, March 5, 2020 - 4:54:20 PM
Long-term archiving on: : Friday, April 2, 2010 - 8:33:15 PM

Identifiers

  • HAL Id : tel-00007132, version 1

Collections

Citation

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⟩

Share

Metrics

Record views

296

Files downloads

429