Product type

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. The pair type is a special case of the dependent pair type, where the type B may depend on the instance picked from A.

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 type₁, ..., type_n is written type₁ * ... * type_n in ML and (type₁,...,type_n) in Haskell. In both these languages, tuples are written (v₁,...,v_n) 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. Product types are the dual of sum types.

Example

An example of a product type is the type of a vector in a vector space or an algebra over a field: the type is a product of a number type, and a direction type. Thus, for example, 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). This is properly indicative of the vector space nature of SI units over the abelian group of dimensions under multiplication, and the field of real numbers -- the SI units form an algebra over a field.

See also

• Quotient type
• Sum type

References

• product type in nLab
• Homotopy Type Theory: Univalent Foundations of Mathematics, The Univalent Foundations Program, Institute for Advanced Study. See section 1.5.