- System F
**System F**, also known as the**polymorphic lambda calculus**or the**second-order lambda calculus**, is atyped lambda calculus . It was discovered independently by thelogician Jean-Yves Girard and thecomputer scientist John C. Reynolds . System F formalizes the notion of parametric polymorphism inprogramming language s.Just as the

lambda calculus has variables ranging over functions, and binders for them,the second-order lambda calculus 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→ Awould be formalized in System F as the judgement

:$vdash\; Lambdaalpha.\; lambda\; x^alpha.x:\; forallalpha.alpha\; o\; alpha$

where α is a

type variable .Under the

Curry-Howard isomorphism , System F corresponds to asecond-order logic .System F, together with even more expressive lambda calculi, can be seen as part of the

lambda cube .**Logic and predicates**The "Boolean" type is defined as:$forallalpha.alpha\; o\; alpha\; o\; alpha$, where α is a

type variable .This produces the following two definitions for the boolean values`TRUE`and`FALSE`:: TRUE := $Lambda\; alpha.lambda\; x^alpha\; lambda\; y^alpha.x$: FALSE := $Lambda\; alpha.lambda\; x^alpha\; lambda\; y^alpha.y$

Then, with these two λ-terms, we can define some logic operators:: AND := $lambda\; x^\{Boolean\}\; lambda\; y^\{Boolean\}.((x\; (Boolean))\; y)\; FALSE$: OR := $lambda\; x^\{Boolean\}\; lambda\; y^\{Boolean\}.((x\; (Boolean))\; TRUE)\; y$: NOT := $lambda\; x^\{Boolean\}.\; ((x\; (Boolean))\; FALSE)\; TRUE$

There really is no need for a "IFTHENELSE" function as one can just use raw Boolean typed terms as decision functions. However, if one is requested:: IFTHENELSE := $Lambda\; alpha.lambda\; x^\{Boolean\}lambda\; y^\{alpha\}lambda\; z^\{alpha\}.((x\; (alpha))\; y)\; z$will do.A "predicate" is a function which returns a boolean value. The most fundamental predicate is

`ISZERO`which returns`TRUE`if and only if its argument is the Church numeral`0`::`ISZERO := λ "n". "n" (λ "x". FALSE) TRUE`**ystem 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 (S) are created using "constructors". These are functions typed as::$K\_1\; ightarrow\; K\_2\; ightarrowdots\; ightarrow\; S$.Recursivity is manifested when $S$ itself appears within one of the types $K\_i$. If you have $m$ of these constructors, you can define the type of $S$ as::$forall\; alpha.(K\_1^1\; [alpha/S]\; ightarrowdots\; ightarrow\; alpha)dots\; ightarrow(K\_1^m\; [alpha/S]\; ightarrowdots\; ightarrow\; alpha)\; ightarrow\; alpha$

For instance, the natural numbers can be defined as an inductive datatype $N$ with constructors:$mathit\{zero\}\; :\; mathrm\{N\}$:$mathit\{succ\}\; :\; mathrm\{N\}\; o\; mathrm\{N\}$The System F type corresponding to this structure is$forall\; alpha.\; alpha\; o\; (alpha\; o\; alpha)\; o\; alpha$. The terms of this type comprise a typed version of the

Church numeral s, the first few of which are::`0 :=`$Lambda\; alpha\; .\; lambda\; x^alpha\; .\; lambda\; f^\{alpha\; oalpha\}\; .\; x$:`1 :=`$Lambda\; alpha\; .\; lambda\; x^alpha\; .\; lambda\; f^\{alpha\; oalpha\}\; .\; f\; x$:`2 :=`$Lambda\; alpha\; .\; lambda\; x^alpha\; .\; lambda\; f^\{alpha\; oalpha\}\; .\; f\; (f\; x)$:`3 :=`$Lambda\; alpha\; .\; lambda\; x^alpha\; .\; lambda\; f^\{alpha\; oalpha\}\; .\; f\; (f\; (f\; x))$If we reverse the order of the curried arguments ("i.e.," $forall\; alpha.\; (alpha\; o\; alpha)\; o\; alpha\; o\; alpha$), then the Church numeral for $n$ is a function that takes a function

`"f"`as argument and returns the $n^\; extrm\{th\}$ power of`"f"`. That is to say, a Church numeral is ahigher-order function -- it takes a single-argument function`"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 undecidable for a Curry-style variant of System F, that is, one that lacks explicit typing annotations. [*http://www.macs.hw.ac.uk/~jbw/research-summary.html*] [*http://www.church-project.org/reports/Wells:APAL-1999-v98-no-note.html*]Wells' 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 manystrongly typed functional programming languages such as Haskell 98 and ML. 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. As of 2008, the Haskell compiler, GHC, goes beyond HM, and now uses System F extended with non-syntactic type equality, for example.**System $F\_omega$**System $F\_1$ is the

simply-typed lambda calculus ; it includes no mappings from types to types. The System F described in this article is technically System $F\_2$; that is, the system wherein all mappings from types to types take arguments which are strictly first-order (not functions themselves).In general, there is a family of systems defined inductively by the "kinds" permitted in each system:

* $F\_1$ does not permit any kinds (only types)

* $F\_n$ permits kinds:

** $star$ (the kind of types) and

** $JRightarrow\; K$ where $Jin\; F\_\{n-1\}$ and $Kin\; 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 $F\_omega$ to be

* $F\_omega\; =\; underset\{1\; leq\; i\}\{igcup\}\; F\_i$

That is, $F\_omega$ is the system which allows functions from types to types where the argument (and result) may be of any order.

Note that although $F\_omega$ 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\_omega$ does not permit mappings from values to types (

Dependent types ), though it does permit mappings from values to values ($lambda$ abstraction), mappings from types to values ($Lambda$ abstraction, sometimes written $forall$) and mappings from types to types ($lambda$ abstraction at the level of types)**References***Girard, Lafont and Taylor, [

*http://www.PaulTaylor.EU/stable/Proofs%2BTypes.html "Proofs and Types"*] . Cambridge University Press, 1989, ISBN 0 521 37181 3.

*J. B. Wells. "Typability and type checking in the second-order lambda-calculus are equivalent and undecidable." In "Proceedings of the 9th AnnualIEEE Symposium on Logic in Computer Science (LICS)," pages 176-185, 1994. [*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*]**External links*** [

*http://www.site.uottawa.ca/~fbinard/Intuitionism/TypeTheory/SystemF/ Summary of System F*] by Franck Binard.

*Wikimedia Foundation.
2010.*