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