Theory
A general algebraic data type is a possibly recursive sum type of product types. Each constructor tags a product type to separate it from others, or if there is only one constructor, the data type is a product type. Further, the parameter types of a constructor are the factors of the product type. A parameterless constructor corresponds to the empty product. If a datatype is recursive, the entire sum of products is wrapped in a recursive type, and each constructor also rolls the datatype into the recursive type.
For example, the Haskell datatype:
data List a = Nil | Cons a (List a)is represented in type theory as with constructors and .
The Haskell List datatype can also be represented in type theory in a slightly different form, as follows: . (Note how the and constructs are reversed relative to the original.) The original formation specified a type function whose body was a recursive type; the revised version specifies a recursive function on types. (We use the type variable to suggest a function rather than a "base type" like, since is like a Greek "f".) Note that we must also now apply the function to its argument type in the body of the type.
For the purposes of the List example, these two formulations are not significantly different; but the second form allows one to express so-called nested data types, i.e., those where the recursive type differs parametrically from the original. (For more information on nested data types, see the works of Richard Bird, Lambert Meertens and Ross Paterson.)
In set theory the equivalent of a sum type is a disjoint union – a set whose elements are pairs consisting of a tag (equivalent to a constructor) and an object of a type corresponding to the tag (equivalent to the constructor arguments).
Read more about this topic: Algebraic Data Type
Famous quotes containing the word theory:
“Won’t this whole instinct matter bear revision?
Won’t almost any theory bear revision?
To err is human, not to, animal.”
—Robert Frost (1874–1963)
“We have our little theory on all human and divine things. Poetry, the workings of genius itself, which, in all times, with one or another meaning, has been called Inspiration, and held to be mysterious and inscrutable, is no longer without its scientific exposition. The building of the lofty rhyme is like any other masonry or bricklaying: we have theories of its rise, height, decline and fall—which latter, it would seem, is now near, among all people.”
—Thomas Carlyle (1795–1881)
“It is not enough for theory to describe and analyse, it must itself be an event in the universe it describes. In order to do this theory must partake of and become the acceleration of this logic. It must tear itself from all referents and take pride only in the future. Theory must operate on time at the cost of a deliberate distortion of present reality.”
—Jean Baudrillard (b. 1929)