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.

...
Wikipedia