System F

For the electronic dance music artist, see Ferry Corsten

System F, also known as the polymorphic lambda calculus or the second-order lambda calculus, is a typed lambda calculus. It was discovered independently by the logician Jean-Yves Girard and the computer scientist John C. Reynolds. System F formalizes the notion of parametric polymorphism in programming languages.

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→ A would be formalized in System F as the judgement

[\vdash \Lambda\alpha. \lambda x^\alpha.x: \forall\alpha.\alpha \to \alpha]

where α is a type variable.

Under the Curry-Howard isomorphism, System F corresponds to a second-order logic.

System F, together with even more expressive lambda calculi, can be seen as part of the lambda cube.

Contents

1 Logic and predicates
2 System F Structures
3 Use in programming languages
4 References
5 External links

Logic and predicates

The Boolean type is defined as: [\forall\alpha.\alpha \to \alpha \to \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^ \lambda y^.((x (Boolean)) y) FALSE]

OR := [\lambda x^ \lambda y^.((x (Boolean)) TRUE) y]

NOT := [\lambda x^. ((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^\lambda y^\lambda z^.((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

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. Suppose you want to create an abstract structure (call it S). The first thing you'll need are constructors. These will be functions whose type will be

[K_1\rightarrow K_2\rightarrow\dots\rightarrow 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]\rightarrow\dots\rightarrow \alpha)\dots\rightarrow(K_1^m[alpha/S]\rightarrow\dots\rightarrow \alpha)\rightarrow \alpha]

For instance, the natural numbers can be defined as an inductive datatype [N] with constructors

[\mathit : \mathrm]

[\mathit : \mathrm \to \mathrm]

The System F type corresponding to this structure is [\forall \alpha. \alpha \to (\alpha \to \alpha) \to \alpha]. The terms of this type comprise a typed version of the Church numerals, the first few of which are:

0 := [\Lambda \alpha . \lambda x^\alpha . \lambda f^ . x]

1 := [\Lambda \alpha . \lambda x^\alpha . \lambda f^ . f x]

2 := [\Lambda \alpha . \lambda x^\alpha . \lambda f^ . f (f x)]

3 := [\Lambda \alpha . \lambda x^\alpha . \lambda f^ . f (f (f x))]

If we reverse the order of the curried arguments (i.e., [\forall \alpha. (\alpha \to \alpha) \to \alpha \to \alpha]), then the Church numeral for [n] is a function that takes a function f as argument and returns the [n^\textrm] 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. [link] [link]

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 many strongly typed functional programming languages such as Haskell and ML.

References

Girard, Lafont and Taylor, 1997. [Proofs and Types]. Cambridge University Press.
J. B. Wells. "Typability and type checking in the second-order lambda-calculus are equivalent and undecidable." In Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (LICS), pages 176-185, 1994. [link]

External links

[Summary of System F] by Frank Binard.

From Wikipedia, the Free Encyclopedia. Original article here. Support Wikipedia by contributing or donating.
All text is available under the terms of the GNU Free Documentation License See Wikipedia Copyrights for details.