System F
System F, also known as the (Girard–Reynolds) polymorphic lambda calculus or the secondorder lambda calculus, is a typed lambda calculus that differs from the simply typed lambda calculus by the introduction of a mechanism of universal quantification over types. System F thus formalizes the notion of parametric polymorphism in programming languages, and forms a theoretical basis for languages such as Haskell and ML. System F was discovered independently by logician JeanYves Girard (1972) and computer scientist John C. Reynolds (1974).
Whereas simply typed lambda calculus has variables ranging over functions, 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 judgment
where is a type variable. The uppercase is traditionally used to denote typelevel functions, as opposed to the lowercase which is used for valuelevel functions. (The superscripted means that the bound x is of type ; the expression after the colon is the type of the lambda expression preceding it.)
As a term rewriting system, System F is 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 secondorder 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.^{[1]}
Contents
Logic and predicates
The type is defined as: , where is a type variable. This means: 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 to be rightassociative.)
The following two definitions for the boolean values and are used, extending the definition of Church booleans:
(Note that the above two functions require three — not two — parameters. 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 ; the universal quantifier binding the α corresponds to the Λ binding the alpha in the lambda expression itself. Also, note that is a convenient shorthand for , but it is not a symbol of System F itself, but rather a "metasymbol". Likewise, and are also "metasymbols", convenient shorthands, of System F "assemblies" (in the Bourbaki sense); otherwise, if such functions could be named (within System F), then there would be no need for the lambdaexpressive apparatus capable of defining functions anonymously.)
Then, with these two terms, we can define some logic operators (which are of type ):
As in Church encodings, there is no need for an IFTHENELSE function as one can just use raw typed terms as decision functions. However, if one is requested:
will do. A predicate is a function which returns a typed value. The most fundamental predicate is ISZERO which returns if and only if its argument is the Church numeral 0:
System F structures
System F allows recursive constructions to be embedded in a natural manner, related to that in MartinLöf's type theory. Abstract structures (S) are created using constructors. These are functions typed as:
 .
Recursivity is manifested when itself appears within one of the types . If you have of these constructors, you can define the type of as:
For instance, the natural numbers can be defined as an inductive datatype with constructors
The System F type corresponding to this structure is . The terms of this type comprise a typed version of the Church numerals, the first few of which are:
 0 :=
 1 :=
 2 :=
 3 :=
If we reverse the order of the curried arguments (i.e., ), then the Church numeral for is a function that takes a function f as argument and returns the ^{th} power of f. That is to say, a Church numeral is a higherorder function – it takes a singleargument function f, and returns another singleargument function.
Use in programming languages
The version of System F used in this article is as an explicitly typed, or Churchstyle, calculus. The typing information contained in λterms makes typechecking straightforward. Joe Wells (1994) settled an "embarrassing open problem" by proving that type checking is undecidable for a Currystyle variant of System F, that is, one that lacks explicit typing annotations.^{[2]}^{[3]}
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 98 and ML. Over time, as the restrictions of HMstyle type systems have become apparent, languages have steadily moved to more expressive logics for their type systems. As of 2008, GHC, a Haskell compiler, goes beyond HM, and now uses System F extended with nonsyntactic type equality.^{[4]} F# is designed from scratch with System F in mind.^{[citation needed]}
System F_{ω}
While System F corresponds to the first axis of the Barendregt's lambda cube, System F_{ω} or the higherorder 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 the kinds permitted in each system:

permits kinds:
 (the kind of types) and
 where and (the kind of functions from types to types, where the argument type is of a lower order)
In the limit, we can define system to be
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 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_{ω} does not permit mappings from values to types (Dependent types), though it does permit mappings from values to values ( abstraction), mappings from types to values ( abstraction, sometimes written ) and mappings from types to types ( abstraction at the level of types)
See also
 Existential types – the existentially quantified counterparts of universal types
 System F_{<:} – extends system F with subtyping
 System U
Notes

^ Girard, JeanYves. "The system F of variable types, fifteen years later". Theoretical Computer Science. 45: 160. doi:10.1016/03043975(86)900447.
However, in [3] it was shown that the obvious rules of conversion for this system, called F by chance, were converging.
 ^ http://www.macs.hw.ac.uk/~jbw/researchsummary.html
 ^ "The Church Project: Typability and type checking in {S}ystem {F} are equivalent and undecidable". 29 September 2007. Archived from the original on 29 September 2007.
 ^ "Commentary/Compiler/FC – GHC". ghc.haskell.org. Retrieved 20160709.
References
 Girard, JeanYves (1971). "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". Proceedings of the Second Scandinavian Logic Symposium. Amsterdam. pp. 63–92. doi:10.1016/S0049237X(08)708437.
 Girard, JeanYves (1972), Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur (Ph.D. thesis) (in French), Université Paris 7.
 Reynolds, John (1974). Towards a Theory of Type Structure.
 Girard, Lafont and Taylor, Proofs and Types. Cambridge University Press, 1989, ISBN 0521371813.
 J. B. Wells. "Typability and type checking in the secondorder lambdacalculus are equivalent and undecidable." In Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 176–185, 1994. [1]
Further reading
 Pierce, Benjamin (2002). Types and Programming Languages. MIT Press. ISBN 0262162091., Chapter 23: Universal Types, and Chapter 25: An ML Implementation of System F
External links
Wikibooks has a book on the topic of: Haskell 
 Summary of System F by Franck Binard.
 System Fω: the workhorse of modern compilers by Greg Morrisett