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:
“Don’t confuse hypothesis and theory. The former is a possible explanation; the latter, the correct one. The establishment of theory is the very purpose of science.”
—Martin H. Fischer (1879–1962)
“There is in him, hidden deep-down, a great instinctive artist, and hence the makings of an aristocrat. In his muddled way, held back by the manacles of his race and time, and his steps made uncertain by a guiding theory which too often eludes his own comprehension, he yet manages to produce works of unquestionable beauty and authority, and to interpret life in a manner that is poignant and illuminating.”
—H.L. (Henry Lewis)
“The whole theory of modern education is radically unsound. Fortunately in England, at any rate, education produces no effect whatsoever. If it did, it would prove a serious danger to the upper classes, and probably lead to acts of violence in Grosvenor Square.”
—Oscar Wilde (1854–1900)