System F (alsopolymorphic lambda calculus orsecond-order lambda calculus) is atyped lambda calculus that introduces, tosimply typed lambda calculus, a mechanism ofuniversal quantification over types. System F formalizesparametric polymorphism inprogramming languages, thus forming a theoretical basis for languages such asHaskell andML. It was discovered independently bylogicianJean-Yves Girard (1972) andcomputer scientistJohn C. Reynolds.

Whereassimply typed lambda calculus has variables ranging over terms, and binders for them, System F additionally has variables ranging overtypes, and binders for them. As an example, the fact that the identity function can have any type of the formA →A would be formalized in System F as the statement

${\displaystyle ⊢\mathrm{\Lambda }\alpha .\lambda x^{\alpha }.x:\mathrm{\forall }\alpha .\alpha \to \alpha }$

where${\displaystyle \alpha }$ is atype variable. The upper-case${\displaystyle \mathrm{\Lambda }}$ is traditionally used to denote type-level functions, as opposed to the lower-case${\displaystyle \lambda }$ which is used for value-level functions. (The superscripted${\displaystyle \alpha }$ means that the bound variablex is of type${\displaystyle \alpha }$; the expression after the colon is the type of the lambda expression preceding it.)

As aterm rewriting system, System F isstrongly normalizing. However,type inference in System F (without explicit type annotations) isundecidable. Under theCurry–Howard isomorphism, System F corresponds tosecond-order propositional intuitionistic logic. System F can be seen as part of thelambda cube, together with even more expressive typed lambda calculi, including those withdependent types.

According to Girard, the "F" inSystem F was picked by chance.^[1]

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

${\displaystyle \frac{\mathrm{\Gamma }⊢M:\mathrm{\forall }\alpha .\sigma }{\mathrm{\Gamma }⊢M\tau :\sigma [\tau /\alpha ]}}$ (1)

${\displaystyle \frac{\mathrm{\Gamma },\alpha \text{type}⊢M:\sigma }{\mathrm{\Gamma }⊢\mathrm{\Lambda }\alpha .M:\mathrm{\forall }\alpha .\sigma }}$ (2)

where${\displaystyle \sigma ,\tau }$ are types,${\displaystyle \alpha }$ is a type variable, and${\displaystyle \alpha \text{type}}$ in the context indicates that${\displaystyle \alpha }$ is bound. The first rule is that of application, and the second is that of abstraction.^[2][3]

The${\displaystyle \mathsf{B}\mathsf{o}\mathsf{o}\mathsf{l}\mathsf{e}\mathsf{a}\mathsf{n}}$ type is defined as:${\displaystyle \mathrm{\forall }\alpha .\alpha \to \alpha \to \alpha }$, where${\displaystyle \alpha }$ is atype variable. This means:${\displaystyle \mathsf{B}\mathsf{o}\mathsf{o}\mathsf{l}\mathsf{e}\mathsf{a}\mathsf{n}}$ 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${\displaystyle \to }$ to beright-associative.)

The following two definitions for the Boolean values${\displaystyle \mathbf{T}}$ and${\displaystyle \mathbf{F}}$ are used, extending the definition ofChurch Booleans:

${\displaystyle \mathbf{T}=\mathrm{\Lambda }\alpha .\lambda x^{\alpha }\lambda y^{\alpha }.x}$

${\displaystyle \mathbf{F}=\mathrm{\Lambda }\alpha .\lambda x^{\alpha }\lambda y^{\alpha }.y}$

(Note that the above two functions requirethree — not two — 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${\displaystyle \mathrm{\forall }\alpha .\alpha \to \alpha \to \alpha }$; the universal quantifier binding the α corresponds to the Λ binding the alpha in the lambda expression itself. Also, note that${\displaystyle \mathsf{B}\mathsf{o}\mathsf{o}\mathsf{l}\mathsf{e}\mathsf{a}\mathsf{n}}$ is a convenient shorthand for${\displaystyle \mathrm{\forall }\alpha .\alpha \to \alpha \to \alpha }$, but it is not a symbol of System F itself, but rather a "meta-symbol". Likewise,${\displaystyle \mathbf{T}}$ and${\displaystyle \mathbf{F}}$ are also "meta-symbols", convenient shorthands, of System F "assemblies" (in theBourbaki 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 thefixed-point combinator, which works around that restriction.)

Then, with these two${\displaystyle \lambda }$-terms, we can define some logic operators (which are of type${\displaystyle \mathsf{B}\mathsf{o}\mathsf{o}\mathsf{l}\mathsf{e}\mathsf{a}\mathsf{n}\to \mathsf{B}\mathsf{o}\mathsf{o}\mathsf{l}\mathsf{e}\mathsf{a}\mathsf{n}\to \mathsf{B}\mathsf{o}\mathsf{o}\mathsf{l}\mathsf{e}\mathsf{a}\mathsf{n}}$):

Note that in the definitions above,${\displaystyle \mathsf{B}\mathsf{o}\mathsf{o}\mathsf{l}\mathsf{e}\mathsf{a}\mathsf{n}}$ is a type argument to${\displaystyle x}$, specifying that the other two parameters that are given to${\displaystyle x}$ are of type${\displaystyle \mathsf{B}\mathsf{o}\mathsf{o}\mathsf{l}\mathsf{e}\mathsf{a}\mathsf{n}}$. As in Church encodings, there is no need for anIFTHENELSE function as one can just use raw${\displaystyle \mathsf{B}\mathsf{o}\mathsf{o}\mathsf{l}\mathsf{e}\mathsf{a}\mathsf{n}}$-typed terms as decision functions. However, if one is requested:

${\displaystyle \mathrm{I}\mathrm{F}\mathrm{T}\mathrm{H}\mathrm{E}\mathrm{N}\mathrm{E}\mathrm{L}\mathrm{S}\mathrm{E}=\mathrm{\Lambda }\alpha .\lambda x^{\mathsf{B}\mathsf{o}\mathsf{o}\mathsf{l}\mathsf{e}\mathsf{a}\mathsf{n}}\lambda y^{\alpha }\lambda z^{\alpha }.x\alpha yz}$

will do.Apredicate is a function which returns a${\displaystyle \mathsf{B}\mathsf{o}\mathsf{o}\mathsf{l}\mathsf{e}\mathsf{a}\mathsf{n}}$-typed value. The most fundamental predicate isISZERO which returns${\displaystyle \mathbf{T}}$ if and only if its argument is theChurch numeral0:

${\displaystyle \mathrm{I}\mathrm{S}\mathrm{Z}\mathrm{E}\mathrm{R}\mathrm{O}=\lambda n^{\mathrm{\forall }\alpha .(\alpha \to \alpha )\to \alpha \to \alpha }.n\mathsf{B}\mathsf{o}\mathsf{o}\mathsf{l}\mathsf{e}\mathsf{a}\mathsf{n}(\lambda x^{\mathsf{B}\mathsf{o}\mathsf{o}\mathsf{l}\mathsf{e}\mathsf{a}\mathsf{n}}.\mathbf{F})\mathbf{T}}$

Furthermore, theexistential quantifier (and therefore existential types) can be implemented in system F by the following:^[4][5]

${\displaystyle \mathrm{\exists }X.A=\mathrm{\forall }Y.(\mathrm{\forall }X.A\to Y)\to Y}$

System F allows recursive constructions to be embedded in a natural manner, related to that inMartin-Löf's type theory. Abstract structures (S) are created usingconstructors. These are functions typed as:

${\displaystyle K_1\to K_2\to \cdots \to S}$.

Recursivity is manifested whenS itself appears within one of the types${\displaystyle K_i}$. If you havem of these constructors, you can define the type ofS as:

${\displaystyle \mathrm{\forall }\alpha .(K_1^1[\alpha /S]\to \cdots \to \alpha )\cdots \to (K_1^m[\alpha /S]\to \cdots \to \alpha )\to \alpha }$

For instance, the natural numbers can be defined as an inductive datatypeN with constructors

The System F type corresponding to this structure is${\displaystyle \mathrm{\forall }\alpha .\alpha \to (\alpha \to \alpha )\to \alpha }$. The terms of this type comprise a typed version of theChurch numerals, the first few of which are:

If we reverse the order of the curried arguments (i.e.,${\displaystyle \mathrm{\forall }\alpha .(\alpha \to \alpha )\to \alpha \to \alpha }$), then the Church numeral forn is a function that takes a functionf as argument and returns then^th power off. That is to say, a Church numeral is ahigher-order function – it takes a single-argument functionf, and returns another single-argument function.

The version of System F used in this article is as an explicitly typed, or Church-style, calculus. The typing information contained in λ-terms makestype-checking straightforward.Joe Wells (1994) settled an "embarrassing open problem" by proving that type checking isundecidable for a Curry-style variant of System F, that is, one that lacks explicit typing annotations.^[6][7]

Wells's result implies thattype 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 manystatically typedfunctional programming languages such asHaskell 98 and theML 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, a Haskell compiler, goes beyond HM (as of 2008) and uses System F extended with non-syntactic type equality;^[8] non-HM features inOCaml's type system includeGADT.^[9][10]

In second-orderintuitionistic logic, the second-order polymorphic lambda calculus (F2) was discovered by Girard (1972) and independently by Reynolds (1974).^[11] Girard proved therepresentation 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.^[11] Reynolds proved theabstraction theorem: that every term in F2 satisfies a logical relation, which can be embedded into the logical relations P2.^[11] Reynolds proved that a Girard projection followed by a Reynolds embedding form the identity, i.e., theGirard–Reynolds isomorphism.^[11]

While System F corresponds to the first axis ofBarendregt'slambda cube,System F_ω or thehigher-order polymorphic lambda calculus combines the first axis (polymorphism) with the second axis (type operators); it is a different, more complex system.

System F_ω can be defined inductively on a family of systems, where induction is based on thekinds permitted in each system:

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

In the limit, we can define system${\displaystyle F_{\omega }}$ to be

• ${\displaystyle F_{\omega }=\bigcup _{1\le i}{F}_i}$

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

Note that although F_ω places no restrictions on theorder of the arguments in these mappings, it does restrict theuniverse of the arguments for these mappings: they must be types rather than values. System F_ω does not permit mappings from values to types (dependent types), though it does permit mappings from values to values (${\displaystyle \lambda }$ abstraction), mappings from types to values (${\displaystyle \mathrm{\Lambda }}$ abstraction), and mappings from types to types (${\displaystyle \lambda }$ abstraction at the level of types).

System F_<:, pronounced "F-sub", is an extension of system F withsubtyping. System F_<: has been of central importance toprogramming language theory since the 1980s because the core offunctional programming languages, like those in theML family, support bothparametric polymorphism andrecord subtyping, which can be expressed inSystem F_<:.^[12][13]

• Existential types — the existentially quantified counterparts of universal types
• System U
• Lambda cube

• Pierce, Benjamin (2002)."V Polymorphism Ch. 23. Universal Types, Ch. 25. An ML Implementation of System F".Types and Programming Languages. MIT Press. pp. 339–362,381–388.ISBN 0-262-16209-1.

Wikibooks has a book on the topic of:Haskell

• Summary of System F by Franck Binard.
• System F_ω: the workhorse of modern compilers byGreg Morrisett

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

• Articles with short description
• Short description matches Wikidata
• CS1 French-language sources (fr)