|
System F - Definition and Overview |
| Related Words: Mo, Aggregation, Algorithm, All, Angle, Arrangement, Array, Attack, Basis, Blueprint, Brand, Calculation, Cast, Character |
|
|
|
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.
|
|
|
