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:
“The human species, according to the best theory I can form of it, is composed of two distinct races, the men who borrow and the men who lend.”
—Charles Lamb (1775–1834)
“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)
“There never comes a point where a theory can be said to be true. The most that one can claim for any theory is that it has shared the successes of all its rivals and that it has passed at least one test which they have failed.”
—A.J. (Alfred Jules)