System F
|
|
- For the electronic dance music artist, see Ferry Corsten
System F is a typed lambda calculus. It is also known as the second-order or polymorphic 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.
External links
- Proofs and Types - New link (http://www.cs.man.ac.uk/~pt/stable/prot.pdf)