Editing System F

{{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>

== 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\mathbin{:}\forall\alpha.\sigma}{\Gamma\vdash M\tau\mathbin{:}\sigma[\tau/\alpha]} }</math> (1)
| align="center" | <math>{\frac{\Gamma,\alpha~\text{type}\vdash M\mathbin{:}\sigma}{\Gamma\vdash\Lambda\alpha.M\mathbin{:}\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 |url=https://www.cs.cmu.edu/~rwh/pfpl/2nded.pdf |title=Practical Foundations for Programming Languages, Second Edition |vauthors=Harper R |author-link=Robert Harper (computer scientist) |pages=142–3}}</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]]. 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]].)

The following two definitions for the boolean values <math>\mathbf{T}</math> and <math>\mathbf{F}</math> are used, extending the definition of [[Church encoding#Church Booleans|Church booleans]]:

: <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]], 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 encoding#Church numerals|Church numeral]] {{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>

==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]]. 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]]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]] – 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]] straightforward.  [[Joe Wells]] (1994) settled an "embarrassing open problem" by proving that type checking is [[decision problem|undecidable]] 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=Ann. Pure Appl. 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]] for System F is impossible.
A restriction of System F known as "[[Hindley–Milner]]", or simply "HM", does have an easy type inference algorithm and is used for many [[statically typed]] [[functional programming languages]] such as [[Haskell (programming language)|Haskell 98]] and the [[ML programming language|ML]] 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. [[Glasgow Haskell Compiler|GHC]], 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]]'s type system include [[generalized algebraic data types|GADT]].<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]], 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]] (2005) [http://homepages.inf.ed.ac.uk/wadler/papers/gr2/gr2.pdf  The Girard-Reynolds Isomorphism (second edition)] [[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 [[Henk Barendregt|Barendregt's]] [[lambda cube]], '''System F<sub>ω</sub>''' or the '''higher-order polymorphic lambda calculus''' combines the first axis (polymorphism) with the second axis ([[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 (type theory)|kind]]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]]), 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]]. System F<sub>&lt;:</sub> has been of central importance to [[programming language theory]] since the 1980s{{citation needed|date=September 2014}} because the core of [[functional programming languages]], like those in the [[ML (programming language)|ML]] family, support both [[parametric polymorphism]] and [[Record (computer science)|record]] 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]]</ref>

== See also ==
* [[Existential types]] — the existentially quantified counterparts of universal types
* [[System U]]
* [[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]] 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]]

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