System F information

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

\vdash \Lambda \alpha .\lambda x^{\alpha }.x:\forall \alpha .\alpha \to \alpha

where $\alpha$ is a type variable. The upper-case $\Lambda$ is traditionally used to denote type-level functions, as opposed to the lower-case $\lambda$ which is used for value-level functions. (The superscripted $\alpha$ means that the bound x is of type $\alpha$ ; 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.^[1]

^ Girard, Jean-Yves (1986). "The system F of variable types, fifteen years later". Theoretical Computer Science. 45: 160. doi:10.1016/0304-3975(86)90044-7. However, in [3] it was shown that the obvious rules of conversion for this system, called F by chance, were converging.

[1] Girard, Jean-Yves (1986). "The system F of variable types, fifteen years later". Theoretical Computer Science. 45: 160. doi:10.1016/0304-3975(86)90044-7. However, in [3] it was shown that the obvious rules of conversion for this system, called F by chance, were converging.

System F information

and 13 Related for: System F information

System F

F

Fourier optics

System

Lambda cube

819 line

Fairchild Channel F

Broadcast television systems

F2FS

Statics

Academic grading in the United States

Superposition principle

Elliptic coordinate system