Editing System F (section)

{{short description|Typed lambda calculus}}
{{For|the electronic trance music artist|Ferry Corsten}}
'''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 language]]s, thus forming a theoretical basis for languages such as [[Haskell (programming language)|Haskell]] and [[ML (programming language)|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

:<math>\vdash \Lambda\alpha. \lambda x^\alpha.x: \forall\alpha.\alpha \to \alpha</math>

where <math>\alpha</math> is a [[type variable]].  The upper-case <math>\Lambda</math> is traditionally used to denote type-level functions, as opposed to the lower-case <math>\lambda</math> which is used for value-level functions. (The superscripted <math>\alpha</math> means that the bound variable ''x'' is of type <math>\alpha</math>; the expression after the colon is the type of the lambda expression preceding it.)

As a [[term rewriting system]], System F is [[Normalization property (lambda-calculus)|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.<ref>{{Cite journal|last=Girard|first=Jean-Yves|title=The system F of variable types, fifteen years later|journal=Theoretical Computer Science|volume=45|page=160|doi=10.1016/0304-3975(86)90044-7|quote=However, in [3] it was shown that the obvious rules of conversion for this system, called F by chance, were converging.|year=1986|doi-access=}}</ref>