全称类型和柯里霍华德同构

大家可能有这样的疑惑，为什么需要将多态的函数类型记成$\forall X. T_1\Rightarrow T_2$的样子呢？

它的原因是，类型系统的推理规则，其实本质上和一个逻辑上的公理系统的推理规则是一样的。

我们可以把一个命题，例如$A\to B$看成是一个类型$A\Rightarrow B$。

他们具有类似的推理规则，即分离规则(有$A$和$A\to B$,则有$B$)和函数应用规则(有$A$类型的实例和$A\Rightarrow B$ 类型的函数, 则可以通过调用函数得到$B$类型的实例)。

类型和命题可以一一对应，因此他们是同构的，这种同构叫做柯里霍华德同构(Curry-Howard Isomorphism)。

逻辑学上的二阶直觉主义逻辑中的$\forall$量词，正和多态的类型同构。

因此，带有类型参数的函数类型，也叫做全称类型。