
System F

System F, also known as the (Girard–Reynolds) polymorphic lambda calculus or the second-order 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 Jean-Yves Girard (1972) and computer scientist John C. Reynolds (1974).
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 judgment
where formula_2 is a type variable. The upper-case formula_3 is traditionally used to denote type-level functions, as opposed to the lower-case formula_4 which is used for value-level functions. (The superscripted formula_2 means that the bound "x" is of type formula_2; 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 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.
Typing rules.
The typing rules of System F are those of simply typed lambda calculus with the addition of the following:
where formula_7 are types, formula_2 is a type variable, and formula_9 in the context indicates that formula_2 is bound. The first rule is that of application, and the second is that of abstraction.
Logic and predicates.
The formula_11 type is defined as:
formula_12, where formula_2 is a type variable. This means: formula_11 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 formula_15 to be right-associative.)
The following two definitions for the boolean values formula_16 and formula_17 are used, extending the definition of Church booleans:
Then, with these two formula_4-terms, we can define some logic operators (which are of type formula_26):
Note that in the definitions above, formula_11 is a type argument to formula_29, specifying that the other two parameters that are given to formula_29 are of type formula_11. As in Church encodings, there is no need for an IFTHENELSE function as one can just use raw formula_11-typed terms as decision functions. However, if one is requested:
will do.
A "predicate" is a function which returns a formula_11-typed value. The most fundamental predicate is ISZERO which returns formula_16 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 Martin-Löf's type theory. Abstract structures (S) are created using "constructors". These are functions typed as:
Recursivity is manifested when formula_38 itself appears within one of the types formula_39. If you have formula_40 of these constructors, you can define the type of formula_38 as:
For instance, the natural numbers can be defined as an inductive datatype formula_43 with constructors
The System F type corresponding to this structure is
formula_46. The terms of this type comprise a typed version of the Church numerals, the first few of which are:
If we reverse the order of the curried arguments ("i.e.," formula_51), then the Church numeral for formula_52 is a function that takes a function "f" as argument and returns the formula_52th power of "f". That is to say, a Church numeral is a higher-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.
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 the 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. GHC a Haskell compiler, goes beyond HM (as of 2008) and uses System F extended with non-syntactic type equality; non-HM features in OCaml's type system include GADT.
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). 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. Reynolds proved the "Abstraction Theorem": that every term in F2 satisfies a logical relation, which can be embedded into the logical relations P2. Reynolds proved that a Girard projection followed by a Reynolds embedding form the identity, i.e., the Girard-Reynolds Isomorphism.
System Fω.
While System F corresponds to the first axis of Barendregt's lambda cube, System Fω or the higher-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 the kinds permitted in each system:
In the limit, we can define system formula_59 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 (formula_4 abstraction), mappings from types to values (formula_3 abstraction) and mappings from types to types (formula_4 abstraction at the level of types)