积类型

积类型表达“同时拥有一份 $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分别以恰好一次和至多一次的上下文纪律约束值使用，并显式隔离可复制资源。则在线性上下文分割下同时交付两个分量，不能无条件复用这些笛卡尔投影规则；二者的差别来自资源纪律，不是换一个乘号而已。