|
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.
|
Example Usage of System |
 |
DavidWaren: But FDR gamed the System to get it upheld anyway. |
 |
reesesteven: Anyone can follow this simple & Hands Free List Building System and Get Paid on complete autopilot... ==> http://www.lilmuse.com/r5.ph.. |
 |
shedd: @pagerduty looks like a useful System, but is a bit expensive, especially when you're already paying for monitoring services... |
|
|
