En los lenguajes de programación y la teoría de tipos , un producto de tipos es otro tipo compuesto en una estructura. Los "operandos" del producto son tipos , y la estructura de un tipo de producto está determinada por el orden fijo de los operandos en el producto. Una instancia de un tipo de producto conserva el orden fijo, pero por lo demás puede contener todas las instancias posibles de sus tipos de datos primitivos . La expresión de una instancia de un tipo de producto será una tupla , y se denomina "tipo de tupla" de expresión. Un producto de tipos es un producto directo de dos o más tipos.
Si solo hay dos tipos de componentes, se puede llamar "tipo de par". Por ejemplo, si dos tipos de componentes A y B son el conjunto de todos los valores posibles de ese tipo, el tipo de producto escrito A × B contiene elementos que son pares (a,b), donde "a" y "b" son instancias de A y B respectivamente. El tipo de par es un caso especial del tipo de par dependiente , donde el tipo B puede depender de la instancia elegida de A.
En muchos lenguajes, los tipos de producto toman la forma de un tipo de registro , para el cual se puede acceder a los componentes de una tupla mediante la etiqueta . En lenguajes que tienen tipos de datos algebraicos , como en la mayoría de los lenguajes de programación funcional , los tipos de datos algebraicos con un constructor son isomorfos a un tipo de producto.
En la correspondencia Curry-Howard , los tipos de productos están asociados con la conjunción lógica (AND) en la lógica .
La noción se extiende directamente al producto de un número finito arbitrario de tipos (un tipo de producto n -ario) y, en este caso, caracteriza las expresiones que se comportan como tuplas de expresiones de los tipos correspondientes. Una forma degenerada del tipo de producto es el tipo unidad : es el producto de ningún tipo .
En los lenguajes de programación de llamada por valor , un tipo de producto puede interpretarse como un conjunto de pares cuyo primer componente es un valor del primer tipo y cuyo segundo componente es un valor del segundo tipo. En resumen, es un producto cartesiano y corresponde a un producto de la categoría de tipos.
La mayoría de los lenguajes de programación funcional tienen una noción primitiva de tipo de producto. Por ejemplo, el producto de tipo 1 , ..., tipo n se escribe type 1* ... *type n en ML y (type 1, ... ,type n) en Haskell . En ambos lenguajes, las tuplas se escriben (v 1, ... ,v n) y los componentes de una tupla se extraen mediante coincidencia de patrones . Además, muchos lenguajes de programación funcional proporcionan tipos de datos algebraicos más generales, que extienden tanto los tipos de producto como los de suma . Los tipos de producto son el dual de los tipos de suma .