System F
Encyclopedia
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 language
s, 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.
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.
, where 
is a type variable
.
This produces the following two definitions for the boolean values
and 
:
Then, with these two
-terms, we can define some logic operators:
There is no need for an IFTHENELSE 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 ISZERO which returns 
if and only if its argument is the Church numeral 0:
.
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 numerals, 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 f as argument and returns the 
th power of f. That is to say, a Church numeral is a higher-order function
– it takes a single-argument function f, and returns another single-argument function.
for a Curry-style variant of System F, that is, one that lacks explicit typing annotations.
Wells' result implies that type inference
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 strongly typed functional programming languages such as Haskell 98
and ML
. 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. As of 2008, GHC
, a Haskell compiler, goes beyond HM, and now uses System F extended with non-syntactic type equality, for example.
, system Fω combines the first axis (polymorphism) with type operators (the second axis); it is a different, more complex system.
System Fω can be defined inductively on a family of systems, where induction is based on the kind
s permitted in each system:
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, sometimes written 
) and mappings from types to types (
abstraction at the level of types)
Typed lambda calculus
A typed lambda calculus is a typed formalism that uses the lambda-symbol 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 type depends on the calculus considered...
that differs from the simply typed lambda calculus
Simply typed lambda calculus
The simply typed lambda calculus , a formof type theory, is a typed interpretation of the lambda calculus with only one type constructor: \to that builds function types. It is the canonical and simplest example of a typed lambda calculus...
by the introduction of a mechanism of universal quantification over types. System F thus formalizes the notion of parametric polymorphism
Parametric polymorphism
In programming languages and type theory, parametric polymorphism is a way to make a language more expressive, while still maintaining full static type-safety. Using parametric polymorphism, a function or a data type can be written generically so that it can handle values identically without...
in programming language
Programming language
A programming language is an artificial language designed to communicate instructions to a machine, particularly a computer. Programming languages can be used to create programs that control the behavior of a machine and/or to express algorithms precisely....
s, and forms a theoretical basis for languages such as Haskell
Haskell (programming language)
Haskell is a standardized, general-purpose purely functional programming language, with non-strict semantics and strong static typing. It is named after logician Haskell Curry. In Haskell, "a function is a first-class citizen" of the programming language. As a functional programming language, the...
and ML. System F was discovered independently by logician Jean-Yves Girard
Jean-Yves Girard
Jean-Yves Girard is a French logician working in proof theory. His contributions include a proof of strong normalization in a system of second-order logic called system F; the invention of linear logic; the geometry of interaction; and ludics...
and computer scientist
Computer scientist
A computer scientist is a scientist who has acquired knowledge of computer science, the study of the theoretical foundations of information and computation and their application in computer systems....
John C. Reynolds
John C. Reynolds
John C. Reynolds is an American computer scientist.John Reynolds studied at Purdue University and then earned a PhD in theoretical physics from Harvard University in 1961. He was Professor of Information science at Syracuse University from 1970 to 1986. Since then he has been Professor of Computer...
.
Whereas simply typed lambda calculus
Simply typed lambda calculus
The simply typed lambda calculus , a formof type theory, is a typed interpretation of the lambda calculus with only one type constructor: \to that builds function types. It is the canonical and simplest example of a 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
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 to some memory locations.Programming languages that...
. The upper-case
is traditionally used to denote type-level functions, as opposed to the lower-case which is used for value-level functions.As a term rewriting system, System F is strongly normalizing
Normalization property (lambda-calculus)
In mathematical logic and theoretical computer science, a rewrite system has the strong normalization property if every term is strongly normalizing; that is, if every sequence of rewrites eventually terminates to a term in normal form...
. 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
Intuitionistic logic
Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...
that uses only universal quantification. System F can be seen as part of the lambda cube
Lambda cube
In mathematical logic and type theory, the λ-cube is a framework for exploring the axes of refinement in Coquand's calculus of constructions, starting from the simply typed lambda calculus as the vertex of a cube placed at the origin, and the calculus of constructions as its diametrically opposite...
, together with even more expressive typed lambda calculi, including those with dependent types.
Logic and predicates
The Boolean type is defined as:, where is a type variableType 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 to some memory locations.Programming languages that...
.
This produces the following two definitions for the boolean values
and :
Then, with these two
-terms, we can define some logic operators:
There is no need for an IFTHENELSE 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 ISZERO which returns if and only if its argument is the Church numeral 0:
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 (S) 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 numerals, the first few of which are:
- 0 :=
- 1 :=
- 2 :=
- 3 :=
If we reverse the order of the curried arguments (i.e.,
), then the Church numeral for is a function that takes a function f as argument and returns the th power of f. That is to say, a Church numeral is a higher-order functionHigher-order function
In mathematics and computer science, higher-order functions, functional forms, or functionals are functions which do at least one of the following:*take one or more functions as an input*output a function...
– it takes a single-argument function f, 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 undecidableDecision problem
In computability theory and computational complexity theory, a decision problem is a question in some formal system with a yes-or-no answer, depending on the values of some input parameters. For example, the problem "given two numbers x and y, does x evenly divide y?" is a decision problem...
for a Curry-style variant of System F, that is, one that lacks explicit typing annotations.
Wells' result implies that type inference
Type inference
Type inference refers to the automatic deduction of the type of an expression in a programming language. If some, but not all, type annotations are already present it is referred to as type reconstruction....
for System F is impossible.
A restriction of System F known as "Hindley–Milner
Hindley–Milner
In type theory, Hindley–Milner is a classical type inference method with parametric polymorphism for the lambda calculus, first described by J. Roger Hindley...
", or simply "HM", does have an easy type inference algorithm and is used for many strongly typed functional programming languages such as Haskell 98
Haskell (programming language)
Haskell is a standardized, general-purpose purely functional programming language, with non-strict semantics and strong static typing. It is named after logician Haskell Curry. In Haskell, "a function is a first-class citizen" of the programming language. As a functional programming language, the...
and ML
ML programming language
ML is a general-purpose functional programming language developed by Robin Milner and others in the early 1970s at the University of Edinburgh, whose syntax is inspired by ISWIM...
. 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. As of 2008, GHC
Glasgow Haskell Compiler
The Glorious Glasgow Haskell Compilation System, more commonly known as the Glasgow Haskell Compiler or GHC, is an open source native code compiler for the functional programming language Haskell. The lead developers are Simon Peyton Jones and Simon Marlow...
, a Haskell compiler, goes beyond HM, and now uses System F extended with non-syntactic type equality, for example.
System Fω
Although System F corresponds to the first axis of the Barendregt's lambda cubeLambda cube
In mathematical logic and type theory, the λ-cube is a framework for exploring the axes of refinement in Coquand's calculus of constructions, starting from the simply typed lambda calculus as the vertex of a cube placed at the origin, and the calculus of constructions as its diametrically opposite...
, system Fω combines the first axis (polymorphism) with type operators (the second axis); it is a different, more complex system.
System Fω can be defined inductively on a family of systems, where induction is based on the kind
Kind (type theory)
In the area of mathematical logic and computer science known as type theory, a kind is the type of a type constructor or, less commonly, the type of a higher-order type operator...
s 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, sometimes written ) and mappings from types to types ( abstraction at the level of types)See also
- Existential types are the existentially quantified counterparts of universal types.
- System F<: extends system F with subtyping, bringing it a lot closer to actual programming languages from the ML family.
External links
- Summary of System F by Franck Binard.