积类型

积类型表达“同时拥有一份 $A$ 和一份 $B$”。构造它必须给出两个分量，使用它可独立投影任一分量；因此信息是累积而非选择性的。把它想成固定字段的二元记录最自然，更多元组只是重复嵌套或一般化。名称来自集合的笛卡尔积，但程序类型还携带求值与相等规则，不能只把它当作无语义的内存布局。

函数

具有类型 $A\times B\to B\times A$。若 $p=(3,\mathsf{true})$，则 ${\pi }_{1}p\to 3$，${\pi }_{2}p\to \mathsf{true}$。

边界是积类型与和类型的混淆：$A\times B$ 的每个值都同时包含两类数据，而 $A+B$ 每次只包含某一分支。若语言有副作用，构造一对时两个分量的求值顺序仍需另行规定；类型本身不决定先算左边还是右边。

积类型支撑元组、记录、函数多返回值和环境结构。记录类型可看作带字段名的有限积，函数多参数也可柯里化或接收一个积类型参数。

在Curry–Howard 对应公理库Curry–Howard 对应Curry–Howard correspondence · Propositions as types把命题对应为类型、证明对应为程序、证明化简对应为程序求值。下，$A\times B$ 对应合取 $A\wedge B$：构造一对就是同时给出两个证明，投影就是取出其中一个。积作为构造子字段的组合方式进入代数数据类型公理库代数数据类型Algebraic data type · Algebraic datatype以有限构造子的和、每个构造子字段的积以及可选递归组合数据形状的类型。；完整的和—积—递归汇总由该页承担。

普通积允许分别投影、从而忽略另一分量。线性 tensor公理库线性类型与仿射类型Linear type · Affine type · Linear and affine types分别以恰好一次和至多一次的上下文纪律约束值使用，并显式隔离可复制资源。则在线性上下文分割下同时交付两个分量，不能无条件复用这些笛卡尔投影规则；二者的差别来自资源纪律，不是换一个乘号而已。