В языках программирования и теории типов произведение типов — это другой, составной, тип в структуре. «Операндами» произведения являются типы , а структура типа произведения определяется фиксированным порядком операндов в произведении. Экземпляр типа произведения сохраняет фиксированный порядок, но в остальном может содержать все возможные экземпляры его примитивных типов данных . Выражение экземпляра типа произведения будет кортежем и называется «типом кортежа» выражения. Произведение типов — это прямое произведение двух или более типов.
Если есть только два типа компонентов, его можно назвать «типом пары». Например, если два типа компонентов A и B являются набором всех возможных значений этого типа, тип продукта, записанный как A × B , содержит элементы, которые являются парами (a,b), где «a» и «b» являются экземплярами A и B соответственно. Тип пары является особым случаем зависимого типа пары , где тип B может зависеть от экземпляра, выбранного из A.
Во многих языках типы продуктов принимают форму типа записи , для которого компоненты кортежа могут быть доступны по метке . В языках, имеющих алгебраические типы данных , как и в большинстве функциональных языков программирования , алгебраические типы данных с одним конструктором изоморфны типу продукта.
В соответствии с Карри–Ховардом типы продуктов связаны с логической конъюнкцией (И) в логике .
Понятие напрямую распространяется на произведение произвольного конечного числа типов ( n -арный тип произведения), и в этом случае оно характеризует выражения, которые ведут себя как кортежи выражений соответствующих типов. Вырожденной формой типа произведения является тип единицы : это произведение ни одного типа .
В языках программирования с вызовом по значению тип продукта можно интерпретировать как набор пар, первый компонент которых является значением в первом типе, а второй компонент — значением во втором типе. Короче говоря, это декартово произведение , и оно соответствует произведению в категории типов.
Большинство функциональных языков программирования имеют примитивное понятие типа продукта. Например, продукт типа 1 , ..., типа n записывается как тип 1* ... *тип n в ML и (тип 1, ... ,тип n) в Haskell . В обоих этих языках кортежи записываются как (v 1, ... ,v n) , а компоненты кортежа извлекаются с помощью сопоставления с образцом . Кроме того, многие функциональные языки программирования предоставляют более общие алгебраические типы данных , которые расширяют как типы продукта, так и типы суммы . Типы продукта являются двойственными типам суммы.