Are you an EPFL student looking for a semester project?
Work with us on data science and visualisation projects, and deploy your project as an app on top of GraphSearch.
Concept
System F
Summary
System F (also polymorphic lambda calculus or second-order lambda calculus) is a typed lambda calculus that introduces, to simply typed lambda calculus, a mechanism of universal quantification over types. System F formalizes parametric polymorphism in programming languages, thus forming a theoretical basis for languages such as Haskell and ML. It was discovered independently by logician Jean-Yves Girard (1972) and computer scientist John C. Reynolds.
Whereas simply typed lambda calculus has variables ranging over terms, and binders for them, System F additionally has variables ranging over types, and binders for them. As an example, the fact that the identity function can have any type of the form A → A would be formalized in System F as the judgement
where is a type variable. The upper-case is traditionally used to denote type-level functions, as opposed to the lower-case which is used for value-level functions. (The superscripted means that the bound x is of type ; the expression after the colon is the type of the lambda expression preceding it.)
As a term rewriting system, System F is strongly normalizing. However, type inference in System F (without explicit type annotations) is undecidable. Under the Curry–Howard isomorphism, System F corresponds to the fragment of second-order intuitionistic logic that uses only universal quantification. System F can be seen as part of the lambda cube, together with even more expressive typed lambda calculi, including those with dependent types.
According to Girard, the "F" in System F was picked by chance.
The typing rules of System F are those of simply typed lambda calculus with the addition of the following:
where are types, is a type variable, and in the context indicates that is bound. The first rule is that of application, and the second is that of abstraction.
The type is defined as:
where is a type variable. This means: is the type of all functions which take as input a type α and two expressions of type α, and produce as output an expression of type α (note that we consider to be right-associative.
Official source
About this result
This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.