积 (类型论)

积类型积集类型论中的类比, 它在简单类型论依值类型论里都可以定义, 且定义是一样的. 注意积类型不是 类型, 即使有时我们认为积类型是 类型的特例.

在类型论中, 积类型的对偶是不交并.

1类型规则

类型 的积记作 .

以下规则基本就是模仿范畴论泛构造.

构造规则

可以直接将 视为由如上构造子生成的归纳类型, 也可以单独给出消去规则.

消去规则

积类型的消去规则有两种风格:

其中:

另一种风格是通过函数类型定义, 也就是 作为归纳类型的情况下的消去规则:

其中:

这种思路非常接近 Curry 化和积类型的 编码. 两者的区别在于极性不同.

2范畴语义

在简单类型论的范畴语义中, 积类型对应对象.

在依值类型论的范畴语义中, 积类型对应俯范畴里的积, 也就是拉回.

术语翻译

积类型英文 product type法文 type produit拉丁文 typus productus