System F (also polymorphic lambda calculus or second-order lambda calculus) is a
typed lambda calculus
A typed lambda calculus is a typed formalism that uses the lambda-symbol (\lambda) to denote anonymous function abstraction. In this context, types are usually objects of a syntactic nature that are assigned to lambda terms; the exact nature of a ...
that introduces, to
simply typed lambda calculus, a mechanism of
universal quantification
In mathematical logic, a universal quantification is a type of quantifier, a logical constant which is interpreted as "given any" or "for all". It expresses that a predicate can be satisfied by every member of a domain of discourse. In other ...
over types. System F formalizes
parametric polymorphism in
programming language
A programming language is a system of notation for writing computer programs. Most programming languages are text-based formal languages, but they may also be graphical. They are a kind of computer language.
The description of a programming ...
s, thus forming a theoretical basis for languages such as
Haskell and
ML. It was discovered independently by
logician Jean-Yves Girard (1972) and
computer scientist
A computer scientist is a person who is trained in the academic study of computer science.
Computer scientists typically work on the theoretical side of computation, as opposed to the hardware side on which computer engineers mainly focus (a ...
John C. Reynolds
John Charles Reynolds (June 1, 1935 – April 28, 2013) was an American computer scientist.
Education and affiliations
John Reynolds studied at Purdue University and then earned a Doctor of Philosophy (Ph.D.) in theoretical physics from Harvard U ...
Whereas
simply typed lambda calculus has variables ranging over terms, 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 judgement
:
where
is a
type variable In type theory and programming languages, a type variable is a mathematical variable ranging over types. Even in programming languages that allow mutable variables, a type variable remains an abstraction, in the sense that it does not correspond t ...
. 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.)
As a
term rewriting system
In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. Such methods may be achieved by rewriting systems (also known as rewrite systems, rewrite engines, or redu ...
, System F is
strongly normalizing
In abstract rewriting, an object is in normal form if it cannot be rewritten any further, i.e. it is irreducible. Depending on the rewriting system, an object may rewrite to several normal forms or none at all. Many properties of rewriting systems ...
. However,
type inference
Type inference refers to the automatic detection of the type of an expression in a formal language. These include programming languages and mathematical type systems, but also natural languages in some branches of computer science and linguistic ...
in System F (without explicit type annotations) is undecidable. Under the
Curry–Howard isomorphism, System F corresponds to the fragment of second-order
intuitionistic logic
Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems ...
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.
According to Girard, the "F" in ''System F'' was picked by chance.
Typing rules
The typing rules of System F are those of simply typed lambda calculus with the addition of the following:
where
are types,
is a type variable, and
in the context indicates that
is bound. The first rule is that of application, and the second is that of abstraction.
Logic and predicates
The
type is defined as:
, where
is a
type variable In type theory and programming languages, a type variable is a mathematical variable ranging over types. Even in programming languages that allow mutable variables, a type variable remains an abstraction, in the sense that it does not correspond t ...
. This means:
is the type of all functions which take as input a type α and two expressions of type α, and produce as output an expression of type α (note that we consider
to be
right-associative.)
The following two definitions for the boolean values
and
are used, extending the definition of
Church booleans:
:
:
(Note that the above two functions require ''three'' — not two — arguments. The latter two should be lambda expressions, but the first one should be a type. This fact is reflected in the fact that the type of these expressions is
; the universal quantifier binding the α corresponds to the Λ binding the alpha in the lambda expression itself. Also, note that
is a convenient shorthand for
, but it is not a symbol of System F itself, but rather a "meta-symbol". Likewise,
and
are also "meta-symbols", convenient shorthands, of System F "assemblies" (in th
Bourbaki sense; otherwise, if such functions could be named (within System F), then there would be no need for the lambda-expressive apparatus capable of defining functions anonymously and for the
fixed-point combinator, which works around that restriction.)
Then, with these two
-terms, we can define some logic operators (which are of type
):
:
Note that in the definitions above,
is a type argument to
, specifying that the other two parameters that are given to
are of type
. As in Church encodings, there is no need for an function as one can just use raw
-typed terms as decision functions. However, if one is requested:
:
will do.
A ''predicate'' is a function which returns a
-typed value. The most fundamental predicate is which returns
if and only if its argument is the
Church numeral
In mathematics, Church encoding is a means of representing data and operators in the lambda calculus. The Church numerals are a representation of the natural numbers using lambda notation. The method is named for Alonzo Church, who first encoded d ...
:
:
System F structures
System F allows recursive constructions to be embedded in a natural manner, related to that in
Martin-Löf's type theory. Abstract structures () are created using ''constructors''. These are functions typed as:
:
.
Recursivity is manifested when itself appears within one of the types
. If you have of these constructors, you can define the type of as:
:
For instance, the natural numbers can be defined as an inductive datatype with constructors
:
The System F type corresponding to this structure is
. The terms of this type comprise a typed version of the
Church numeral
In mathematics, Church encoding is a means of representing data and operators in the lambda calculus. The Church numerals are a representation of the natural numbers using lambda notation. The method is named for Alonzo Church, who first encoded d ...
s, the first few of which are:
:
If we reverse the order of the curried arguments (''i.e.,''
), then the Church numeral for is a function that takes a function as argument and returns the
th power of . That is to say, a Church numeral is a
higher-order function
In mathematics and computer science, a higher-order function (HOF) is a function that does at least one of the following:
* takes one or more functions as arguments (i.e. a procedural parameter, which is a parameter of a procedure that is itse ...
– it takes a single-argument function , and returns another single-argument function.
Use in programming languages
The version of System F used in this article is as an explicitly typed, or Church-style, calculus. The typing information contained in λ-terms makes
type-checking straightforward.
Joe Wells (1994) settled an "embarrassing open problem" by proving that type checking is
undecidable for a Curry-style variant of System F, that is, one that lacks explicit typing annotations.
Wells's result implies that
type inference
Type inference refers to the automatic detection of the type of an expression in a formal language. These include programming languages and mathematical type systems, but also natural languages in some branches of computer science and linguistic ...
for System F is impossible.
A restriction of System F known as "
Hindley–Milner", or simply "HM", does have an easy type inference algorithm and is used for many
statically typed functional programming languages such as
Haskell 98 and the
ML family. Over time, as the restrictions of HM-style type systems have become apparent, languages have steadily moved to more expressive logics for their type systems.
GHC a Haskell compiler, goes beyond HM (as of 2008) and uses System F extended with non-syntactic type equality; non-HM features in
OCaml
OCaml ( , formerly Objective Caml) is a general-purpose, multi-paradigm programming language
Programming paradigms are a way to classify programming languages based on their features. Languages can be classified into multiple paradigms.
...
's type system include
GADT.
The Girard-Reynolds Isomorphism
In second-order
intuitionistic logic
Intuitionistic logic, sometimes more generally called constructive logic, refers to systems of symbolic logic that differ from the systems used for classical logic by more closely mirroring the notion of constructive proof. In particular, systems ...
, the second-order polymorphic lambda calculus (F2) was discovered by Girard (1972) and independently by Reynolds (1974).
Girard proved the ''Representation Theorem'': that in second-order intuitionistic predicate logic (P2), functions from the natural numbers to the natural numbers that can be proved total, form a projection from P2 into F2.
Reynolds proved the ''Abstraction Theorem'': that every term in F2 satisfies a logical relation, which can be embedded into the logical relations P2.
Reynolds proved that a Girard projection followed by a Reynolds embedding form the identity, i.e., the Girard-Reynolds Isomorphism.
[ Philip Wadler (2005]
The Girard-Reynolds Isomorphism (second edition)
University of Edinburgh
The University of Edinburgh ( sco, University o Edinburgh, gd, Oilthigh Dhùn Èideann; abbreviated as ''Edin.'' in post-nominals) is a public research university based in Edinburgh, Scotland. Granted a royal charter by King James VI in 1 ...
Programming Languages and Foundations at Edinburgh
/ref>
System Fω
While System F corresponds to the first axis of Barendregt's lambda cube, System Fω or the higher-order polymorphic lambda calculus combines the first axis (polymorphism) with the second axis ( type operators); it is a different, more complex system.
System Fω can be defined inductively on a family of systems, where induction is based on the kinds permitted in each system:
* permits kinds:
** (the kind of types) and
** where and (the kind of functions from types to types, where the argument type is of a lower order)
In the limit, we can define system to be
*
That is, Fω is the system which allows functions from types to types where the argument (and result) may be of any order.
Note that although Fω places no restrictions on the ''order'' of the arguments in these mappings, it does restrict the ''universe'' of the arguments for these mappings: they must be types rather than values. System Fω does not permit mappings from values to types ( Dependent types), though it does permit mappings from values to values ( abstraction), mappings from types to values ( abstraction), and mappings from types to types ( abstraction at the level of types).
System F<:
System F<:, pronounced "F-sub", is an extension of system F with subtyping. System F<: has been of central importance to programming language theory
Programming language theory (PLT) is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of formal languages known as programming languages. Programming language theory is clos ...
since the 1980s because the core of functional programming languages, like those in the ML family, support both parametric polymorphism and record subtyping, which can be expressed in System F<:.[, Chapter 26: ]Bounded quantification
In type theory, bounded quantification (also bounded polymorphism or constrained genericity) refers to universal or existential quantifiers which are restricted ("bounded") to range only over the subtypes of a particular type. Bounded quantifica ...
See also
* Existential types — the existentially quantified counterparts of universal types
* System U
Notes
References
*
* .
*
*
Postscript version
Further reading
*
External links
{{Wikibooks, Haskell
Summary of System F
by Franck Binard.
System Fω: the workhorse of modern compilers
by Greg Morrisett
1971 in computing
1974 in computing
Lambda calculus
Type theory
Polymorphism (computer science)
Logic