From Wikipedia, the free encyclopedia

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

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

The Boolean type is defined as: , where α is a type variable. This produces the following two definitions for the boolean values TRUE and FALSE:

TRUE := Λα.λx^αλy^α.x

FALSE := Λα.λx^αλy^α.y

Then, with these two λ-terms, we can define some logic operators:

AND := λx^Booleanλy^Boolean.((x(Boolean))y)FALSE

OR := λx^Booleanλy^Boolean.((x(Boolean))TRUE)y

NOT := λ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 := Λα.λx^Booleanλy^αλz^α.((x(α))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 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 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:

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

zero:N

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 n is a function that takes a function f as argument and returns the n^th 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.

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. [1] [2]

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.

• 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. [3]

• Summary of System F by Franck Binard.