System F Article Index for
System 		Articles about
System F 		Website Links For
System 		 

Information About

System F
  CATEGORIES ABOUT SYSTEM F
   
lambda calculus
   
type theory
   
APPAREL
BABY
BEAUTY
BOOKS
CAR TOYS
CELL PHONES
DVD'S
ELECTRONICS
GOURMET FOOD
GROCERIES
HEALTH & PERSONAL
HOME & GARDEN
JEWELRY
MUSIC
MUSIC INSTRUMENTS
OFFICE PRODUCTS
SOFTWARE
SPORTING GOODS
TOOLS & HARDWARE
TOYS
VIDEO GAMES
SHOPPING HOME
MORE SHOPPING...



''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 Language s.

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

: dash \Lambda\alpha. \lambda x^\alpha.x: orall\alpha.\alpha o \alpha

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 .


LOGIC AND PREDICATES

The ''Boolean'' type is defined as:
orall\alpha.\alpha o \alpha o \alpha, where α is a Type Variable .
This produces the following two definitions for the boolean values TRUE and FALSE:

: TRUE := \Lambda \alpha.\lambda x^\alpha \lambda y^\alpha.x
: FALSE := \Lambda \alpha.\lambda x^\alpha \lambda y^\alpha.y

Then, with these two λ-terms, we can define some logic operators:
: AND := \lambda x^{Boolean} \lambda y^{Boolean}.((x (Boolean)) y) FALSE
: OR := \lambda x^{Boolean} \lambda y^{Boolean}.((x (Boolean)) TRUE) y
: NOT := \lambda x^{Boolean}. ((x (Boolean)) FALSE) TRUE

There really is no need for a ''IFTHENELSE'' function as one can just use raw Boolean typed terms as decision functions. However, if one is requested:
: IFTHENELSE := \Lambda \alpha.\lambda x^{Boolean}\lambda y^{\alpha}\lambda z^{\alpha}.((x (\alpha)) y) z
will do.
A ''predicate'' is a function which returns a boolean value. The most fundamental predicate is ISZERO which returns TRUE if and only if its argument is the Church numeral 0:
: ISZERO := λ ''n''. ''n'' (λ ''x''. FALSE) TRUE


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 . Suppose you want to create an abstract structure (call it S). The first thing you'll need are constructors. These will be functions whose type will be
:K_1 ightarrow K_2 ightarrow\dots ightarrow S.

Recursivity is manifested when S itself appears within one of the types K_i. If you have m of these constructors, you can define the type of S as:
: orall \alpha.(K_1^1[\alpha/S] ightarrow\dots ightarrow \alpha)\dots ightarrow(K_1^m[\alpha/S] ightarrow\dots ightarrow \alpha) ightarrow \alpha

For instance, the natural numbers can be defined as an inductive datatype N with constructors
:\mathit{zero} : \mathrm{N}
:\mathit{succ} : \mathrm{N} o \mathrm{N}
The System F type corresponding to this structure is
orall \alpha. \alpha o (\alpha o \alpha) o \alpha. The terms of this type comprise a typed version of the Church Numeral s, the first few of which are:
: 0 := \Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha o\alpha} . x
: 1 := \Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha o\alpha} . f x
: 2 := \Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha o\alpha} . f (f x)
: 3 := \Lambda \alpha . \lambda x^\alpha . \lambda f^{\alpha o\alpha} . f (f (f x))

If we reverse the order of the curried arguments (''i.e.,'' orall \alpha. (\alpha o \alpha) o \alpha o \alpha), then the Church numeral for n is a function that takes a function ''f'' as argument and returns the n^ extrm{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.


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. [http://www.church-project.org/reports/Wells:APAL-1999-v98-no-note.html

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 and ML .


REFERENCES

  • Girard, Lafont and Taylor, 1997. ''Proofs and Types'' . Cambridge University Press.

  • J. B. Wells. "Typability and type checking in the second-order lambda-calculus are equivalent and undecidable." In ''Proceedings of the 9th Annual IEEE Symposium on Logic in Computer Science (LICS),'' pages 176-185, 1994. {Link without Title}



EXTERNAL LINKS