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 function – it takes a single-argument function f, and returns another single-argument function.
Read more about this topic: System F
Famous quotes containing the words system and/or structures:
“Intimately concerned as we are with the system of Europe, it does not follow that we are therefore called upon to mix ourselves on every occasion, with a restless and meddling activity, in the concerns of the nations which surround us.”
—George Canning (1770–1827)
“The philosopher believes that the value of his philosophy lies in its totality, in its structure: posterity discovers it in the stones with which he built and with which other structures are subsequently built that are frequently better—and so, in the fact that that structure can be demolished and yet still possess value as material.”
—Friedrich Nietzsche (1844–1900)