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:
“We find ourselves under the government of a system of political institutions, conducing more essentially to the ends of civil and religious liberty, than any of which the history of former times tells us.”
—Abraham Lincoln (1809–1865)
“If there are people who feel that God wants them to change the structures of society, that is something between them and their God. We must serve him in whatever way we are called. I am called to help the individual; to love each poor person. Not to deal with institutions. I am in no position to judge.”
—Mother Teresa (b. 1910)