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
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 |
|
