System F, also known as the (Girard–Reynolds) polymorphic lambda calculus or the second-order lambda calculus, is a typed lambda calculus that differs from the simply typed lambda calculus by the introduction of a mechanism of universal quantification over types. System F thus formalizes the notion of parametric polymorphism in programming languages, and forms a theoretical basis for languages such as Haskell and ML. System F was discovered independently by logician Jean-Yves Girard and computer scientist John C. Reynolds.
Whereas simply typed lambda calculus has variables ranging over functions, and binders for them, System F additionally 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 judgment
where is a type variable. The upper-case is traditionally used to denote type-level functions, as opposed to the lower-case which is used for value-level functions. (The superscripted means that the bound x is of type ; the expression after the colon is the type of the lambda expression preceding it. The colon has a function analogous to that of the double colon in Haskell.)
As a term rewriting system, System F is strongly normalizing. Type inference in System F (without explicit type annotations) is undecidable however. Under the Curry–Howard isomorphism, System F corresponds to the fragment of second-order intuitionistic logic that uses only universal quantification. System F can be seen as part of the lambda cube, together with even more expressive typed lambda calculi, including those with dependent types.
Read more about System F: Logic and Predicates, System F Structures, Use in Programming Languages, System Fω
Famous quotes containing the words system f and/or system:
“Predatory capitalism created a complex industrial system and an advanced technology; it permitted a considerable extension of democratic practice and fostered certain liberal values, but within limits that are now being pressed and must be overcome. It is not a fit system for the mid- twentieth century.”
—Noam Chomsky (b. 1928)
“There are obvious places in which government can narrow the chasm between haves and have-nots. One is the public schools, which have been seen as the great leveler, the authentic melting pot. That, today, is nonsense. In his scathing study of the nation’s public school system entitled “Savage Inequalities,” Jonathan Kozol made manifest the truth: that we have a system that discriminates against the poor in everything from class size to curriculum.”
—Anna Quindlen (b. 1952)