Тип-произведение (также Π-тип, произведение типов; англ. product type) — конструкция в языках программирования и интуиционистской теории типов, тип данных, построенный как декартово произведение исходных типов; другими словами — кортеж типов, или «кортеж как тип» . Использованные типы и порядок их следования определяют сигнатуру[англ.] типа-произведения; порядок следования объектов в создаваемом кортеже сохраняется на протяжении его времени жизни согласно заданной сигнатуре.
Например, если типы A
и B
представляют собой множества значений a
и b
соответственно, то составленное из них декартово произведение записывается как A
×B
, и полученный тип-произведение представляет собой всё множество возможных пар (a,b)
.
В языках, использующих вызов по значению, тип-произведение может интерпретироваться как произведение в категории типов. В соответствии Карри-Ховарда типы-произведения соответствуют конъюнкции в логике (операции AND
).
Частный случай произведения двух типов часто называют «парой» или более точно «упорядоченной парой». Произведение произвольного конечного количества типов называется «n-арным типом-произведением» или «кортежем из n типов». В русскоязычной литературе также присутствует вариант наименования «упорядоченная энка» (обобщение от «двойка», «тройка» и т. д.), лингвистически построенный по аналогии с английским термином «tuple» (см. кортеж (англ.)).
Вырожденная форма типа-произведения — произведение нуля типов — представляет собой единичный тип[англ.] (англ. unit type, «тип юнит»), то есть тип, представленный единственным значением. Системы типов некоторых языков (например, Python) могут предусматривать один или несколько уникальных единичных типов, не совместимых с типом кортежа из нуля элементов.
Типы-произведения встроены в большинство функциональных языков программирования. Например, произведение type1× … × typen записывается как type1 *
… *
typen в ML или как (
type1,
…,
typen)
в Haskell. В обоих языках кортежи записываются как (
v1,
…,
vn)
и их компоненты извлекаются посредством сопоставления с образцом. В дополнение к этому большинство функциональных языков предоставляет алгебраические типы данных, расширяющие понятия как типа-произведения, так и типа-суммы. Алгебраические типы, заданные единственным конструктором, изоморфны типам-произведениям.