算术表达式和类型范畴之间的一点点关系

然所谓困苦者，乃锻炼之谓，非使之柔弱以自苦也。

偶然看到的。

• 首先这是类型范畴中的两个经典情况。左侧对应了类型 c 可以有两个态射分别到类型 a 和类型 b，右侧对应了类型 a 和类型 b 都有一个态射到类型 c。

• 实际上，在编程语言中，左侧对应了$Pair<a,b>$ 的情况，右侧则对应了$Either\;a\;b$ 的情况。（好吧我 C++ 和 Haskell 混用一下）

  同时，在数学中，左侧对应了$*$ 的运算，右侧对应了$+$ 的运算。这怎么理解呢？

• 首先可以考虑两个特殊的类型：$Unit$ 和$Void$。根据我的理解，type 就是值的集合，是范畴中的对象。而 Unit 就是只有唯一一个值的类型，Void 就是没有一个值的类型，分别对应了$1$ 和$0$。

  然后 pair 显然是有结合律的，即有$Pair<a,Pair<b,c>>\sim Pai<Pair<a,b>,c>$，其中$\sim$ 表示 isomorphism，是一一映射的。而 Either 也是有结合律的，于是我们可以把它们看作乘法和加法。实际上，这两个范畴是同构的。

  $$Pair<a,Unit>\sim a\Leftrightarrow a*1=a\\ Pair<a,Void>\sim Void\Leftrightarrow a*0=0\\ Either\;a\;Unit=Left\;a|Unit\sim Maybe\;a=a+1\\ Either\;a\;Void\sim a=a+0$$

  注意，$a+1$ 就是我们的 Maybe，只不过构造子$Just$ 其实就是$Left$，而只有一个值的类型$Nothing$ 其实就是$Unit$。

• 所以再重申一遍：

  $$(a,b)\sim a*b\\ Either\;a\;b\sim a+b\\ Unit\sim 1\\ Void\sim 0$$

  于是我们可以用它来解非常厉害的东西。譬如：

  $$L(a)=1+a*L(a)$$

  这是啥意思呢，其实可以转化：

  $$List\;a=Either\;Nil\;(a,List\;a)=Nil|(a,List\;a)$$

  其中$Nil$ 也是只有一个值的对象，起到 Unit 的作用。我们发现，这个东西其实就是列表的定义。

  通过解方程，有$L(a)=\frac{1}{1-a}=\sum_{n=0}^{\infin}a^n$，所以：

  $$List\;a=1+a+a*a+a*a*a+...\\ =Nil|a|(a,a)|((a,a)a)|...$$

  实际上就生成了列表类型。

• 最后说明下，其实 Unit 的同名有很多，后面不跟类型的类型构造子都可以看作 Unit，例如（Nothing，Nil 等）。但是 Void 一般只有叫 Void。