形式陈述

给定类型 $A,B$$A,B$，积类型 $A\times B$$A\times B$ 的值是有序对。其典型类型规则为

$$ \frac{\Gamma\vdash t_1:A\qquad\Gamma\vdash t_2:B}{\Gamma\vdash (t_1,t_2):A\times B}, \qquad \frac{\Gamma\vdash t:A\times B}{\Gamma\vdash \pi_i t:A_i}\;(i=1,2). $$$$\frac{\mathrm{\Gamma }⊢t_1:A\mathrm{\Gamma }⊢t_2:B}{\mathrm{\Gamma }⊢(t_1,t_2):A\times B},\frac{\mathrm{\Gamma }⊢t:A\times B}{\mathrm{\Gamma }⊢{\pi }_{i}t:A_i}(i=1,2).$$

计算规则给 $\pi_1(v_1,v_2)\to v_1$${\pi }_1(v_1,v_2)\to v_1$、$\pi_2(v_1,v_2)\to v_2$${\pi }_2(v_1,v_2)\to v_2$；相应的 $\eta$$\eta$ 原理表达一个积值由其两个投影完全决定。零元积是单位类型，有限多元组可由二元积嵌套表示。

直觉

积类型要求同时拥有一个 $A$$A$ 值和一个 $B$$B$ 值；构造时提供两部分，使用时分别投影。

例子与边界

坐标、记录和返回多个结果都可建模为积。类型 int × bool 的值如 (3,true)，与 bool × int 一般不同。积不是集合论意义上的交集，也不同于和类型：后者只携带两种分支之一。严格求值和惰性求值会影响组成部分何时计算，但不改变基本类型规则。

推论与应用

积类型是记录、环境、状态对和多参数函数柯里化的基础。它与笛卡尔积对应，并在类型范畴中满足从任意对象到积的映射由两个投影分量唯一决定的泛性质。

参考资料

• Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002，Ch. 11, products, tuples, and records。
• Robert Harper, Practical Foundations for Programming Languages, 2nd ed., Cambridge University Press, 2016，Ch. 11, product types。