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 languages, thus forming a theoretical basis for languages such as Haskell and 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
\vdashΛ\alpha.λx\alpha.x:\forall\alpha.\alpha\to\alpha
where
\alpha
Λ
λ
\alpha
\alpha
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.[1]
The typing rules of System F are those of simply typed lambda calculus with the addition of the following:
M\taun{:}\sigma[\tau/\alpha]}} |
|
where
\sigma,\tau
\alpha
\alpha~type
\alpha
The
Boolean
\forall\alpha.\alpha\to\alpha\to\alpha
\alpha
Boolean
\to
The following two definitions for the boolean values
T
F
T=Λ\alpha{.}λx\alphaλy\alpha{.}x
F=Λ\alpha{.}λx\alphaλy\alpha{.}y
(Note that the above two functions require three - 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
\forall\alpha.\alpha\to\alpha\to\alpha
Boolean
\forall\alpha.\alpha\to\alpha\to\alpha
T
F
Then, with these two
λ
Boolean → Boolean → Boolean
\begin{align} AND&=λxBooleanλyBoolean{.}xBooleanyF\\ OR&=λxBooleanλyBoolean{.}xBooleanTy\\ NOT&=λxBoolean{.}xBooleanFT\end{align}
Note that in the definitions above,
Boolean
x
x
Boolean
Boolean
IFTHENELSE=Λ\alpha.λxBooleanλy\alphaλz\alpha.x\alphayz
Boolean
T
ISZERO=λn\forall{.}nBoolean(λxBoolean{.}F)T
System F allows recursive constructions to be embedded in a natural manner, related to that in Martin-Löf's type theory. Abstract structures are created using constructors. These are functions typed as:
K1 → K2 → ... → S
Recursivity is manifested when itself appears within one of the types
Ki
\forall
1[\alpha/S] → ... → | |
\alpha.(K | |
1 |
m[\alpha/S] → ... → | |
\alpha)... → (K | |
1 |
\alpha) → \alpha
For instance, the natural numbers can be defined as an inductive datatype with constructors
\begin{align} zero&:N\\ succ&:N → N \end{align}
\forall\alpha.\alpha\to(\alpha\to\alpha)\to\alpha
\begin{align} 0&:=Λ\alpha.λx\alpha.λf\alpha\to\alpha.x\\ 1&:=Λ\alpha.λx\alpha.λf\alpha\to\alpha.fx\\ 2&:=Λ\alpha.λx\alpha.λf\alpha\to\alpha.f(fx)\\ 3&:=Λ\alpha.λx\alpha.λf\alpha\to\alpha.f(f(fx)) \end{align}
If we reverse the order of the curried arguments (i.e.,
\forall\alpha.(\alpha → \alpha) → \alpha → \alpha
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.[4] [5]
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;[6] non-HM features in OCaml's type system include GADT.[7] [8]
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.[9]
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:
Fn
\star
J ⇒ K
J\inFn-1
K\inFn
In the limit, we can define system
F\omega
F\omega=\underset{1\leqi}{cup}Fi
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 (
λ
Λ
λ
System F<:, pronounced "F-sub", is an extension of system F with subtyping. System F<: has been of central importance to programming language theory since the 1980s because the core of functional programming languages, like those in the ML family, support both parametric polymorphism and record subtyping, which can be expressed in System F<:.[10] [11]