# System F

> Mediated Wiki article. Canonical URL: https://mediated.wiki/source/System_F
> Markdown URL: https://mediated.wiki/source/System_F.md
> Source: https://en.wikipedia.org/wiki/System_F
> Source revision: 1353196841
> License: Creative Commons Attribution-ShareAlike 4.0 International (https://creativecommons.org/licenses/by-sa/4.0/)

{{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](/source/typed_lambda_calculus) that introduces, to [simply typed lambda calculus](/source/simply_typed_lambda_calculus), a mechanism of [universal quantification](/source/universal_quantification) over types. System F formalizes [parametric polymorphism](/source/parametric_polymorphism) in [programming language](/source/programming_language)s, thus forming a theoretical basis for languages such as [Haskell](/source/Haskell_(programming_language)) and [ML](/source/ML_(programming_language)). It was discovered independently by [logician](/source/logician) [Jean-Yves Girard](/source/Jean-Yves_Girard) (1972) and [computer scientist](/source/computer_scientist) [John C. Reynolds](/source/John_C._Reynolds).

Whereas [simply typed lambda calculus](/source/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](/source/identity_function) can have any type of the form ''A'' → ''A'' would be formalized in System F as the statement

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

where <math>\alpha</math> is a [type variable](/source/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](/source/term_rewriting_system), System F is [strongly normalizing](/source/Normalization_property_(lambda-calculus)). However, [type inference](/source/type_inference) in System F (without explicit type annotations) is [undecidable](/source/undecidable_problem). Under the [Curry–Howard isomorphism](/source/Curry%E2%80%93Howard_isomorphism), System F corresponds to [second-order propositional intuitionistic logic](/source/second-order_propositional_logic). System F can be seen as part of the [lambda cube](/source/lambda_cube), together with even more expressive typed lambda calculi, including those with [dependent types](/source/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](/source/Theoretical_Computer_Science_(journal))|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>

== Typing rules ==

The typing rules of System F are those of simply typed lambda calculus with the addition of the following:

{| align="center" cellpadding="9"
| align="center" | <math>{\frac{\Gamma\vdash M : \forall\alpha.\sigma}{\Gamma\vdash M\tau : \sigma[\tau/\alpha]} }</math> (1)
| align="center" | <math>{\frac{\Gamma,\alpha~\text{type}\vdash M : \sigma}{\Gamma\vdash\Lambda\alpha.M : \forall\alpha.\sigma}}</math> (2)
|}

where <math>\sigma, \tau</math> are types, <math>\alpha</math> is a type variable, and <math>\alpha~\text{type}</math> in the context indicates that <math>\alpha</math> is bound. The first rule is that of application, and the second is that of abstraction.<ref>{{cite web |author-link=Robert Harper (computer scientist) |title=Practical Foundations for Programming Languages, Second Edition |url=https://www.cs.cmu.edu/~rwh/pfpl.html |pages=142–3 |vauthors=Harper R}}</ref><ref>{{cite web |url=http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/lectnotes_vol1.pdf |title=Proofs of Programs and Formalisation of Mathematics |vauthors=Geuvers H, Nordström B, Dowek G |page=51}}</ref>

== Logic and predicates ==

The <math>\mathsf{Boolean}</math> type is defined as:
<math>\forall\alpha.\alpha \to \alpha \to \alpha</math>, where <math>\alpha</math> is a [type variable](/source/type_variable). This means: <math>\mathsf{Boolean}</math> is the type of all functions which take as input a type &alpha; and two expressions of type &alpha;, and produce as output an expression of type &alpha; (note that we consider <math>\to</math> to be [right-associative](/source/right-associative).)

The following two definitions for the Boolean values <math>\mathbf{T}</math> and <math>\mathbf{F}</math> are used, extending the definition of [Church Booleans](/source/Church_encoding):

: <math>\mathbf{T} = \Lambda\alpha{.}\lambda x^{\alpha} \lambda y^\alpha{.}x</math> <!-- These didn't render without the {}-wrapped around the . -->
: <math>\mathbf{F} = \Lambda\alpha{.}\lambda x^{\alpha} \lambda y^{\alpha}{.}y</math>

(Note that the above two functions require ''three'' &mdash; not two &mdash; arguments. The latter two should be lambda expressions, but the first one should be a type. This fact is reflected in the fact that the type of these expressions is <math>\forall\alpha.\alpha \to \alpha \to \alpha</math>; the universal quantifier binding the &alpha; corresponds to the &Lambda; binding the alpha in the lambda expression itself. Also, note that <math>\mathsf{Boolean}</math> is a convenient shorthand for <math>\forall\alpha.\alpha \to \alpha \to \alpha</math>, but it is not a symbol of System F itself, but rather a "meta-symbol". Likewise, <math> \mathbf{T}</math> and <math> \mathbf{F}</math> are also "meta-symbols", convenient shorthands, of System F "assemblies" (in the [https://books.google.com/books?id=IL-SI67hjI4C&q=Nicolas+Bourbaki Bourbaki sense]); otherwise, if such functions could be named (within System F), then there would be no need for the lambda-expressive apparatus capable of defining functions anonymously and for the [fixed-point combinator](/source/fixed-point_combinator), which works around that restriction.)

Then, with these two <math>\lambda</math>-terms, we can define some logic operators (which are of type <math> \mathsf{Boolean} \rightarrow \mathsf{Boolean} \rightarrow \mathsf{Boolean}</math>):
: <math>\begin{align}
\mathrm{AND} &= \lambda x^{\mathsf{Boolean}} \lambda y^{\mathsf{Boolean}}{.} x \, \mathsf{Boolean} \, y\, \mathbf{F}\\
\mathrm{OR}  &= \lambda x^{\mathsf{Boolean}} \lambda y^{\mathsf{Boolean}}{.} x \, \mathsf{Boolean} \, \mathbf{T}\, y\\
\mathrm{NOT} &= \lambda x^{\mathsf{Boolean}}{.} x \, \mathsf{Boolean} \, \mathbf{F}\, \mathbf{T} 
\end{align}</math>

Note that in the definitions above, <math>\mathsf{Boolean}</math> is a type argument to <math>x</math>, specifying that the other two parameters that are given to <math>x</math> are of type <math>\mathsf{Boolean}</math>. As in Church encodings, there is no need for an {{mono|IFTHENELSE}} function as one can just use raw <math>\mathsf{Boolean}</math>-typed terms as decision functions. However, if one is requested:
: <math>\mathrm{IFTHENELSE} = \Lambda \alpha.\lambda x^{\mathsf{Boolean}}\lambda y^{\alpha}\lambda z^{\alpha}. x \alpha y z </math>
will do.
A ''predicate'' is a function which returns a <math>\mathsf{Boolean}</math>-typed value. The most fundamental predicate is {{mono|ISZERO}} which returns <math>\mathbf{T}</math> if and only if its argument is the [Church numeral](/source/Church_encoding) {{mono|0}}:
: <math>\mathrm{ISZERO} = \lambda n^{\forall \alpha. (\alpha \rightarrow \alpha) \rightarrow \alpha \rightarrow \alpha}{.}n \, \mathsf{Boolean} \, (\lambda x^{\mathsf{Boolean}}{.}\mathbf{F})\, \mathbf{T}</math>

Furthermore, the [existential quantifier](/source/existential_quantifier) (and therefore existential types) can be implemented in system F by the following:<ref>Xavier Leroy, Programming = proving? The Curry-Howard correspondence today, Lectures at College de France, Lecture 2, p. 15, 2018-11-21 https://xavierleroy.org/CdF/2018-2019/2.pdf</ref><ref>{{Cite web |title=CS 4110: Programming Languages and Logics - Lecture 26: Existential Types |url=https://www.cs.cornell.edu/courses/cs4110/2018fa/lectures/lecture26.pdf |date=2018 |url-status=live |archive-url=https://web.archive.org/web/20250926100907/https://www.cs.cornell.edu/courses/cs4110/2018fa/lectures/lecture26.pdf |archive-date=2025-09-26 |access-date=2025-11-08 |website=Cornell Ann S. Bowers College of Computing and Information Science |publisher=Department of Computer Science, Cornell University |language=en}}</ref>

: <math> \exists X. A = \forall Y. (\forall X. A \rightarrow Y) \rightarrow Y</math>

==System F structures==

System F allows recursive constructions to be embedded in a natural manner, related to that in [Martin-Löf's type theory](/source/Martin-L%C3%B6f's_type_theory). Abstract structures ({{mvar|S}}) are created using ''constructors''. These are functions typed as:
:<math>K_1\rightarrow K_2\rightarrow\dots\rightarrow S</math>.

Recursivity is manifested when {{mvar|S}} itself appears within one of the types <math>K_i</math>. If you have {{mvar|m}} of these constructors, you can define the type of {{mvar|S}} as:
:<math>\forall \alpha.(K_1^1[\alpha/S]\rightarrow\dots\rightarrow \alpha)\dots\rightarrow(K_1^m[\alpha/S]\rightarrow\dots\rightarrow \alpha)\rightarrow \alpha</math>

For instance, the natural numbers can be defined as an inductive datatype {{mvar|N}} with constructors
: <math>\begin{align}
\mathit{zero} &: \mathrm{N}\\
\mathit{succ} &: \mathrm{N} \rightarrow \mathrm{N}
\end{align}</math>
The System F type corresponding to this structure is
<math>\forall \alpha. \alpha \to (\alpha \to \alpha) \to \alpha</math>. The terms of this type comprise a typed version of the [Church numeral](/source/Church_numeral)s, the first few of which are:
: <math>\begin{align}
0 &:= \Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha\to\alpha} . x\\
1 &:= \Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha\to\alpha} . f x\\
2 &:= \Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha\to\alpha} . f (f x)\\
3 &:= \Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha\to\alpha} . f (f (f x))
\end{align}</math>

If we reverse the order of the curried arguments (''i.e.,'' <math>\forall \alpha. (\alpha \rightarrow \alpha) \rightarrow \alpha \rightarrow \alpha</math>), then the Church numeral for {{mvar|n}} is a function that takes a function {{mvar|f}} as argument and returns the {{mvar|n}}<sup>th</sup> power of {{mvar|f}}. That is to say, a Church numeral is a [higher-order function](/source/higher-order_function) – it takes a single-argument function {{mvar|f}}, and returns another single-argument function.

==Use in programming languages==

The version of System F used in this article is as an explicitly typed, or Church-style, calculus. The typing information contained in λ-terms makes [type-checking](/source/type-checking) straightforward. [Joe Wells](/source/Joe_Wells) (1994) settled an "embarrassing open problem" by proving that type checking is [undecidable](/source/decision_problem) for a Curry-style variant of System F, that is, one that lacks explicit typing annotations.<ref>{{cite web |url=http://www.macs.hw.ac.uk/~jbw/research-summary.html |title= Joe Wells's Research Interests |date=2005-01-20 |publisher=Heriot-Watt University |first=J.B. |last=Wells }}</ref><ref>{{cite journal |first=J.B. |last=Wells |title=Typability and type checking in System F are equivalent and undecidable |journal=[Annals of Pure and Applied Logic](/source/Annals_of_Pure_and_Applied_Logic) |volume=98 |issue=1–3 |pages=111–156 |year=1999 |doi=10.1016/S0168-0072(98)00047-5 |doi-access=free }}{{cite web|url=http://www.church-project.org/reports/Wells:APAL-1999-v98-no-note.html|title=The Church Project: Typability and type checking in {S}ystem {F} are equivalent and undecidable|date=29 September 2007|url-status=dead|archive-url=https://web.archive.org/web/20070929211126/http://www.church-project.org/reports/Wells:APAL-1999-v98-no-note.html|archive-date=29 September 2007}}</ref>

Wells's result implies that [type inference](/source/type_inference) for System F is impossible.
A restriction of System F known as "[Hindley–Milner](/source/Hindley%E2%80%93Milner)", or simply "HM", does have an easy type inference algorithm and is used for many [statically typed](/source/statically_typed) [functional programming languages](/source/functional_programming_languages) such as [Haskell 98](/source/Haskell_(programming_language)) and the [ML](/source/ML_programming_language) family. Over time, as the restrictions of HM-style type systems have become apparent, languages have steadily moved to more expressive logics for their type systems. [GHC](/source/Glasgow_Haskell_Compiler), a Haskell compiler, goes beyond HM (as of 2008) and uses System F extended with non-syntactic type equality;<ref>{{Cite web|url=https://gitlab.haskell.org/ghc/ghc/wikis/commentary/compiler/fc|title=System FC: equality constraints and coercions|website=gitlab.haskell.org|access-date=2019-07-08}}</ref> non-HM features in [OCaml](/source/OCaml)'s type system include [GADT](/source/generalized_algebraic_data_types).<ref>{{cite web|title=OCaml 4.00.1 release notes|date=2012-10-05|access-date=2019-09-23|url=https://ocaml.org/releases/4.00.1.html|website=ocaml.org}}</ref><ref>{{cite web|title=OCaml 4.09 reference manual|date=2012-09-11|access-date=2019-09-23|url=http://caml.inria.fr/pub/docs/manual-ocaml-4.09/manual033.html#s%3Agadts}}</ref>

==The Girard–Reynolds isomorphism==
In second-order [intuitionistic logic](/source/intuitionistic_logic), the second-order polymorphic lambda calculus (F2) was discovered by Girard (1972) and independently by Reynolds (1974).<ref name=gr2 /> Girard proved the ''representation theorem'': that in second-order intuitionistic predicate logic (P2), functions from the natural numbers to the natural numbers that can be proved total, form a projection from P2 into F2.<ref name=gr2 /> Reynolds proved the ''abstraction theorem'': that every term in F2 satisfies a logical relation, which can be embedded into the logical relations P2.<ref name=gr2 /> Reynolds proved that a Girard projection followed by a Reynolds embedding form the identity, i.e., the '''Girard–Reynolds isomorphism'''.<ref name=gr2>[Philip Wadler](/source/Philip_Wadler) (2005) [http://homepages.inf.ed.ac.uk/wadler/papers/gr2/gr2.pdf  The Girard-Reynolds Isomorphism (second edition)] [University of Edinburgh](/source/University_of_Edinburgh), [http://wcms.inf.ed.ac.uk/lfcs/research/groups-and-projects/pl/programming-research-at-lfcs  Programming Languages and Foundations at Edinburgh]</ref>

== System F<sub>ω</sub> ==
While System F corresponds to the first axis of [Barendregt's](/source/Henk_Barendregt) [lambda cube](/source/lambda_cube), '''System F<sub>ω</sub>''' or the '''higher-order polymorphic lambda calculus''' combines the first axis (polymorphism) with the second axis ([type operator](/source/type_operator)s); it is a different, more complex system.

System F<sub>ω</sub> can be defined inductively on a family of systems, where induction is based on the [kind](/source/Kind_(type_theory))s permitted in each system:

* <math>F_n</math> permits kinds:
** <math>\star</math> (the kind of types) and
** <math>J\Rightarrow K</math> where <math>J\in F_{n-1}</math> and <math>K\in F_n</math> (the kind of functions from types to types, where the argument type is of a lower order)

In the limit, we can define system <math>F_\omega</math> to be

* <math>F_\omega = \underset{1 \leq i}{\bigcup} F_i</math>

That is, F<sub>ω</sub> is the system which allows functions from types to types where the argument (and result) may be of any order.

Note that although F<sub>ω</sub> places no restrictions on the ''order'' of the arguments in these mappings, it does restrict the ''universe'' of the arguments for these mappings: they must be types rather than values. System F<sub>ω</sub> does not permit mappings from values to types ([dependent types](/source/dependent_types)), though it does permit mappings from values to values (<math>\lambda</math> abstraction), mappings from types to values (<math>\Lambda</math> abstraction), and mappings from types to types (<math>\lambda</math> abstraction at the level of types).

==System F<sub>&lt;:</sub> ==
'''System F<sub>&lt;:</sub>''', pronounced "F-sub", is an extension of system F with [subtyping](/source/subtyping). System F<sub>&lt;:</sub> has been of central importance to [programming language theory](/source/programming_language_theory) since the 1980s because the core of [functional programming languages](/source/functional_programming_languages), like those in the [ML](/source/ML_(programming_language)) family, support both [parametric polymorphism](/source/parametric_polymorphism) and [record](/source/Record_(computer_science)) subtyping, which can be expressed in '''System F<sub>&lt;:</sub>'''.<ref>{{cite conference
  | first = Luca
  | last = Cardelli |author2=Martini, Simone |author3=Mitchell, John C. |author4=Scedrov, Andre
  | title = An extension of system F with subtyping
  | book-title = Information and Computation, vol. 9
  | pages = 4–56
  | year = 1994
  | location = North Holland, Amsterdam
  | doi = 10.1006/inco.1994.1013
| doi-access = free
  }}</ref><ref>{{cite book|last=Pierce|first=Benjamin|title=Types and Programming Languages|publisher=MIT Press|date=2002|isbn=978-0-262-16209-8}}, Chapter 26: [Bounded quantification](/source/Bounded_quantification)</ref>

== See also ==
* [Existential types](/source/Existential_types) — the existentially quantified counterparts of universal types
* [System U](/source/System_U)
* [Lambda cube](/source/Lambda_cube)

==Notes==
{{Reflist}}

==References==
{{refbegin}}
*{{cite conference
  | first = Jean-Yves | last = Girard | author-link = Jean-Yves Girard
  | title = Une Extension de l'Interpretation de Gödel à l'Analyse, et son Application à l'Élimination des Coupures dans l'Analyse et la Théorie des Types
  | book-title = Proceedings of the Second Scandinavian Logic Symposium
  | date = 1971
  | location = Amsterdam
  | pages = 63–92
  | doi = 10.1016/S0049-237X(08)70843-7
  }}
* {{citation
 | last = Girard | first = Jean-Yves
 | author-link = Jean-Yves Girard 
 | year = 1972
 | title = Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur
 | type = Ph.D. thesis
 | publisher = Université Paris 7
 | language = fr
}}.
*{{cite conference
  | first = John | last = Reynolds | author-link = John C. Reynolds
  | title = Towards a Theory of Type Structure
  | date = 1974
  | url = https://kilthub.cmu.edu/articles/journal_contribution/Towards_a_Theory_of_Type_Structure/6611015/files/12103187.pdf
  }}
*{{cite book |first1=Jean-Yves |last1=Girard |first2=Yves |last2=Lafont |first3=Paul |last3=Taylor |title=Proofs and Types |url=http://www.PaulTaylor.EU/stable/Proofs%2BTypes.html |date=1989 |publisher=Cambridge University Press |isbn=978-0-521-37181-0}}
*{{cite conference |first=J. B. |last=Wells |chapter=Typability and type checking in the second-order lambda-calculus are equivalent and undecidable |title=Proceedings of the 9th Annual [IEEE](/source/IEEE) [Symposium on Logic in Computer Science](/source/Symposium_on_Logic_in_Computer_Science) (LICS) |pages=176–185 |year=1994 |doi= 10.1109/LICS.1994.316068|isbn=0-8186-6310-3}} [http://www.macs.hw.ac.uk/~jbw/papers/Wells:Typability-and-Type-Checking-in-the-Second-Order-Lambda-Calculus-Are-Equivalent-and-Undecidable:LICS-1994.ps.gz Postscript version]
{{refend}}

== Further reading ==
* {{cite book |last=Pierce |first=Benjamin |title=Types and Programming Languages |publisher=MIT Press |date=2002 |isbn=0-262-16209-1 |chapter=V Polymorphism Ch. 23. Universal Types, Ch. 25. An ML Implementation of System F |chapter-url=https://books.google.com/books?id=ti6zoAC9Ph8C&pg=PA340 |pages=339–362, 381–388}}

{{Clear}}

==External links==
{{Wikibooks|Haskell}}
*[http://www.site.uottawa.ca/~fbinard/Intuitionism/TypeTheory/SystemF/ Summary of System F] by Franck Binard.
*[https://web.archive.org/web/20140917015759/http://www.eecs.harvard.edu/~greg/cs256sp2005/lec16.txt System F<sub>&omega;</sub>: the workhorse of modern compilers] by [Greg Morrisett](/source/Greg_Morrisett)

Category:1971 in computing
Category:1974 in computing
Category:Lambda calculus
Category:Type theory
Category:Polymorphism (computer science)
Category:Logic

---
Adapted from the Wikipedia article [System F](https://en.wikipedia.org/wiki/System_F) by Wikipedia contributors ([contributor history](https://en.wikipedia.org/wiki/System_F?action=history)). Available under [Creative Commons Attribution-ShareAlike 4.0 International](https://creativecommons.org/licenses/by-sa/4.0/). Changes may have been made.