製品タイプ

プログラミング言語と型理論では、型の積は構造内の別の複合型です。積の「オペランド」は型であり、積型の構造は積内のオペランドの固定順序によって決まります。積型のインスタンスは固定順序を保持しますが、それ以外の場合は、その基本データ型のすべての可能なインスタンスを含めることができます。積型のインスタンスの式はタプルになり、式の「タプル型」と呼ばれます。型の積は、2 つ以上の型の 直接の積です。

コンポーネント タイプが 2 つしかない場合は、「ペア タイプ」と呼ぶことができます。たとえば、2 つのコンポーネント タイプAとB がそのタイプで可能なすべての値の集合である場合、積の型A × Bには、ペア (a,b) である要素が含まれます。ここで、「a」と「b」は、それぞれAとBのインスタンスです。ペア タイプは、依存ペア タイプの特殊なケースであり、タイプB はAから選択されたインスタンスに依存する場合があります。

多くの言語では、積型はレコード型の形式をとり、タプルのコンポーネントにはラベルでアクセスできます。ほとんどの関数型プログラミング言語と同様に、代数データ型を持つ言語では、1 つのコンストラクタを持つ代数データ型は積型と同型です。

カリー・ハワード対応では、積型は論理における論理積(AND) に関連付けられます。

この概念は、任意の有限個の型の積（n項積型）に直接拡張され、この場合、対応する型の式の組として動作する式を特徴付けます。積型の退化した形式は単位型です。これは型の積ではありません。

値渡しプログラミング言語では、積型は、最初のコンポーネントが最初の型の値であり、2 番目のコンポーネントが 2 番目の型の値であるペアのセットとして解釈できます。つまり、これは直積であり、型のカテゴリの 積に対応します。

ほとんどの関数型プログラミング言語には、積型という基本的な概念があります。たとえば、型₁、...、型_nの積は、 MLではtype ₁* ... *type _nと記述され、Haskellではtype ₁ ... type _nと記述されます。これらの言語の両方で、タプルはv ₁ ... v _nと記述され、タプルのコンポーネントはパターン マッチングによって抽出されます。さらに、多くの関数型プログラミング言語では、積型と和型の両方を拡張する、より一般的な代数データ型が提供されています。積型は和型の双対です。 (,,)(,,)

• 積（圏論）
• デカルト積
• 記録（コンピュータサイエンス）
• 構造体（Cプログラミング言語）
• 合計型
• 商型

• nラボの製品タイプ
• ホモトピー型理論: 数学のユニバレント基礎、ユニバレント基礎プログラム、高等研究所。セクション 1.5 を参照してください。