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 f, system and/or structures:
“Predatory capitalism created a complex industrial system and an advanced technology; it permitted a considerable extension of democratic practice and fostered certain liberal values, but within limits that are now being pressed and must be overcome. It is not a fit system for the mid- twentieth century.”
—Noam Chomsky (b. 1928)
“If mothers are to be successful in achieving their child-rearing goals, they must have the inner freedom to find their own value system and within that system to find what is acceptable to them and what is not. This means leaving behind the anxiety, but also the security, of simplistic good-bad formulations and deciding for themselves what they want to teach their children.”
—Elaine Heffner (20th century)
“The American who has been confined, in his own country, to the sight of buildings designed after foreign models, is surprised on entering York Minster or St. Peter’s at Rome, by the feeling that these structures are imitations also,—faint copies of an invisible archetype.”
—Ralph Waldo Emerson (1803–1882)