这真的只是一种巧合吗？

命题与类型

一个函数的类型可以是 A -> B -> A 。

一个命题的类型可以是 $\alpha \to \beta \to \alpha$ 。

可以发现，这两个类型是类似的。

类型 A 类似于命题 $\alpha$ 。

函数 -> 类似于蕴含 $\to$ 。

实际上这是柯里-霍华德同构。

定义

柯里-霍华德同构揭示了计算机程序和数学证明之间的紧密联系。

类型即命题，程序即证明。

也就是函数的类型相当于命题，函数的实现相当于证明。这在 Coq 中体现得很明显。

用 be5 大大一针见血的解释来说就是

Lambda 演算同构为 Gentzen 的自然演绎

  • 函数调用就是蕴含消除
  • 函数抽象就是蕴含介入
  • 参数多态就是全称量化
  • 模板类型就是谓词
  • 结构类型就是合取
  • 联合类型就是析取
  • 收参数但不返回就是否定
  • 高洋上的 call/cc 就是双重否定消除

简述

函数调用的规则是
$$
{\Gamma\vdash t:\sigma\to\tau\quad\Gamma\vdash u:\sigma}\over{\Gamma\vdash t\,u : \tau}
$$
结果从 $\sigma\to\tau$ 变成 $\tau$ ，少了蕴含 $\to$ 所以称为蕴含消除。

相应的函数调用的逆操作函数抽象的规则是
$$
{\Gamma,x:\sigma\vdash t:\tau}\over{\Gamma\vdash \lambda x : \sigma.t : \sigma \to \tau}
$$
结果从 $\tau$ 变成 $\sigma\to\tau$ ，多了蕴含 $\to$ 所以称为蕴含介入。

参数多态实际上是对于某个参数不限制类型，相当于逻辑量词 $\forall$ ，也就是全称量化。

联合类型，例如 Maybe Int ，表示可能是 Int 或者是 Nothing 。关系是或，也就是析取。

相应地，结构类型表示可以同时是多个类型，关系是且，也就是合取。

对于接受参数而不返回的函数，或者返回 Unit 的函数，实际上类似于 $A \to \bot$ ，返回一个底。

CPS 转换对应的是双重否定转换，也就是双重否定介入。

相应地，call/cc 对应的是双重否定消除。