In programming languages and type theory, a product of types is another, compounded, type in a structure. The "operands" of the product are types, and the structure of a product type is determined by the fixed order of the operands in the product. An instance of a product type retains the fixed order, but otherwise may contain all possible instances of its primitive data types. The expression of an instance of a product type will be a tuple, and is called a "tuple type" of expression. A product of types is a direct product of two or more types.
If there are only two component types, it can be called a "pair type". For example, if two component types A and B are the set of all possible values that type, the product type written A × B contains elements that are pairs (a,b), where "a" and "b" are instances of A and B respectively.
In many languages, product types take the form of a record type, for which the components of a tuple can be accessed by label. In languages that have algebraic data types, as in most functional programming languages, algebraic data types with one constructor are isomorphic to a product type.
In the Curry-Howard correspondence, product types are associated with logical conjunction (AND) in logic.
The notion directly extends to the product of an arbitrary finite number of types (a n-ary product type), and in this case, it characterizes the expressions which behave as tuples of expressions of the corresponding types. A degenerated form of product type is the unit type: it is the product of no types.
In call-by-value programming languages, a product type can be interpreted as a set of pairs whose first component is a value in the first type and whose second component is a value in the second type. In short, it is a cartesian product and it corresponds to a product in the category of types.
Most functional programming languages have a primitive notion of product type. For instance, the product of type1, ..., typen is written type1
* typen in ML and
) in Haskell. In both these languages, tuples are written
) and the components of a tuple are extracted by pattern-matching. Additionally, many functional programming languages provide more general algebraic data types, which extend both product and sum types.
The brochure for the International System of Units starts out in section 1.1 saying "The value of a quantity is generally expressed as the product of a number and a unit", and also presents the unit product of a Newton and a meter with the product notation of mathematics: Newton meter (N m or N · m).
Other articles related to "type, types, product, product types, product type":
... a correspondence between formal proof calculi and type systems for models of computation ... One at the level of formulas and types that is independent of which particular proof system or model of computation is considered, and one at the level of proofs and programs which ... At the level of formulas and types, the correspondence says that implication behaves the same as a function type, conjunction as a "product" type (this may be called a ...
... 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 ...
1950s, made by Librascope, was of this type, as was the principal computer in the Mk ... adjacent side is some fraction that is the product of 1 the distance from the vertex, and 2 the magnitude of the opposite side ... The second input variable in this type of multiplier positions a slotted plate perpendicular to the adjacent side ...
Famous quotes containing the words type and/or product:
“To play safe, I prefer to accept only one type of power: the power of art over trash, the triumph of magic over the brute.”
—Vladimir Nabokov (18991977)
“The end product of child raising is not only the child but the parents, who get to go through each stage of human development from the other side, and get to relive the experiences that shaped them, and get to rethink everything their parents taught them. The get, in effect, to reraise themselves and become their own person.”
—Frank Pittman (20th century)