🏠Homepage🏠 | ⭐Star me on GitHub⭐
前置技能：ADT，构造演算
构造演算中包含一种 * → □ 的函数，这种函数的类型被称为 Π 类型。名字很奇怪，这个类型和 π 毫无关系的啊。实际上这个名字是这么来的：
首先构造一个 Π 类型的函数 F: T → U ，在其定义域 T 中任取一个值 x 那么可以构造类型 F(x) ，那么实际上可以对定义域中每个值都这么操作并且把构造出的类型全部统统放入一个有名元组中
(x_0: F(x_0), x_1: F(x_1), ... , x_n: F(x_n))
这样的定义实际上是和原来的函数等价的，而且这个元组的类型实际上就是一个 ADT 中的积类型
F(x_0) * F(x_1) * ... * F(x_n)
用数学的连乘符号可以表示为
Π_{x: T} F(x)
这里有个 Π 所以它就被称为 Π 类型。
设值 x: T ，和 π 类型函数 F: T → U 那么元组 (x, F(x)) 的类型就是 Σ 类型。实际上有了上面的例子，这里也挺好理解的，对于类型 T 的所有 x 可以构造出
x_0: F(x_0) | x_1: F(x_1) | ... | x_n: F(x_n)
这个类型和那个元组的类型是等价的，而它就是 ADT 中的和类型
F(x_0) + F(x_1) + ... + F(x_n)
用数学的求和符号可以表示为
Σ_{x: T} F(x)
所以它就被称为 Σ 类型。
题外话：个人感觉这样命名类型挺离谱的，拿个符号就来命名，本来符号意思就多，放在这里一眼看上去真猜不出来是啥意思，我觉得叫总积/求和类型都看上去好理解些。