- 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
- <math>\vdash \Lambda\alpha. \lambda x^\alpha.x: \forall\alpha.\alpha \to \alpha</math>
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 |
Logic and predicates
The Boolean type is defined as: <math>\forall\alpha.\alpha \to \alpha \to \alpha</math>, where α is a type variable. This produces the following two definitions for the boolean values TRUE and FALSE:
- TRUE := <math>\Lambda \alpha.\lambda x^\alpha \lambda y^\alpha.x</math>
- FALSE := <math>\Lambda \alpha.\lambda x^\alpha \lambda y^\alpha.y</math>
Then, with these two λ-terms, we can define some logic operators:
- AND := <math>\lambda x^{Boolean} \lambda y^{Boolean}.((x (Boolean)) y) FALSE</math>
- OR := <math>\lambda x^{Boolean} \lambda y^{Boolean}.((x (Boolean)) TRUE) y</math>
- NOT := <math>\lambda x^{Boolean}. ((x (Boolean)) FALSE) TRUE </math>
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 := <math>\Lambda \alpha.\lambda x^{Boolean}\lambda y^{\alpha}\lambda z^{\alpha}.((x (\alpha)) y) z </math>
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. Abstract structures (S) are created using constructors. These are functions typed as:
- <math>K_1\rightarrow K_2\rightarrow\dots\rightarrow S</math>.
Recursivity is manifested when <math>S</math> itself appears within one of the types <math>K_i</math>. If you have <math>m</math> of these constructors, you can define the type of <math>S</math> as:
- <math>\forall \alpha.(K_1^1[\alpha/S]\rightarrow\dots\rightarrow \alpha)\dots\rightarrow(K_1^m[\alpha/S]\rightarrow\dots\rightarrow \alpha)\rightarrow \alpha</math>
For instance, the natural numbers can be defined as an inductive datatype <math>N</math> with constructors
- <math>\mathit{zero} : \mathrm{N}</math>
- <math>\mathit{succ} : \mathrm{N} \to \mathrm{N}</math>
The System F type corresponding to this structure is <math>\forall \alpha. \alpha \to (\alpha \to \alpha) \to \alpha</math>. The terms of this type comprise a typed version of the Church numerals, the first few of which are:
- 0 := <math>\Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha\to\alpha} . x</math>
- 1 := <math>\Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha\to\alpha} . f x</math>
- 2 := <math>\Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha\to\alpha} . f (f x)</math>
- 3 := <math>\Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha\to\alpha} . f (f (f x))</math>
If we reverse the order of the curried arguments (i.e., <math>\forall \alpha. (\alpha \to \alpha) \to \alpha \to \alpha</math>), then the Church numeral for <math>n</math> is a function that takes a function f as argument and returns the <math>n^\textrm{th}</math> 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. [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.
System <math>F_\omega</math>
System <math>F_1</math> is the simply-typed lambda calculus; it includes no mappings from types to types. The System F described in this article is technically System <math>F_2</math>; that is, the system wherein all mappings from types to types take arguments which are strictly first-order (not functions themselves). In general, there is a family of systems defined inductively by the kinds permitted in each system:
- <math>F_1</math> does not permit any kinds (only types)
- <math>F_n</math> permits kinds:
- <math>\star</math> (the kind of types) and
- <math>J\Rightarrow K</math> where <math>J\in F_{n-1}</math> and <math>K\in F_n</math> (the kind of functions from types to types, where the argument type is of a lower order)
In the limit, we can define system <math>F_\omega</math> to be
- <math>F_\omega = \underset{1 \leq i}{\bigcup} F_i</math>
That is, <math>F_\omega</math> is the system which allows functions from types to types where the argument (and result) may be of any order. Note that although <math>F_\omega</math> 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 <math>F_\omega</math> does not permit mappings from values to types (Dependent types), though it does permit mappings from values to values (<math>\lambda</math> abstraction), mappings from types to values (<math>\Lambda</math> abstraction, sometimes written <math>\forall</math>) and mappings from types to types (<math>\lambda</math> abstraction at the level of types)
References
- Girard, Lafont and Taylor, Proofs and Types. Cambridge University Press, 1989, ISBN 0 521 37181 3.
- 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]
External links
- Summary of System F by Franck Binard.
