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:
“Hygiene is the corruption of medicine by morality. It is impossible to find a hygienest who does not debase his theory of the healthful with a theory of the virtuous.... The true aim of medicine is not to make men virtuous; it is to safeguard and rescue them from the consequences of their vices.”
—H.L. (Henry Lewis)
“Osteopath—One who argues that all human ills are caused by the pressure of hard bone upon soft tissue. The proof of his theory is to be found in the heads of those who believe it.”
—H.L. (Henry Lewis)
“Frankly, these days, without a theory to go with it, I can’t see a painting.”
—Tom Wolfe (b. 1931)