Clojure的规格是否与Wadler的命题相当？

Question

Wadler写了一篇惊人的论文:作为类型的命题 - 他谈到了Howard-Curry的对应关系,你可以根据程序的类型来检查程序的行为.(对于给定的语言子集).

最近,Rich Hickey发布了Clojure规范,用于定义数据和功能规范.

这里的评论员写道:

从Wadler我们有道具≅类型,规格≅道具 - >类型ergo可以做静态规格/合同/类型检查.

我的问题是:Clojure的规格是否等同于Wadler的命题？

Answer 1

定义术语

作为类型的命题专门讨论了自然演绎和简单类型 Lambda 演算 (STLC) 之间存在的同构，这两种形式分别适用于逻辑和编程语言。这意味着当您在 STLC 中编程时，您可以将程序转换为逻辑命题。

例如，这些是等效的：

(a -> b) -> a -> b

P implies Q
P
therefore Q

第一个是函数的类型签名，第二个是逻辑命题。现在，当您“Clojure 的规范等同于 Wadler 的主张吗？”时 你问的是“我们可以将 Clojure 规范转换成逻辑语句吗？” 或者由于同构，“我们可以将 clojure 规范转换为 STLC 吗？”

缺乏对等性

规范允许我们使用任何和所有 Clojure谓词。这使得规范变得非常灵活，但这也是看到规范不是命题的关键。

使 STLC 作为逻辑起作用的关键特征之一是所有项都减少，或者换句话说，STLC 中的所有程序都会终止。Clojure 没有这个属性，很容易编写出永远不会终止的 Clojure 程序。任何编程语言要想成为逻辑一致的，就必须具有这种终止性，因为“非终止”就相当于逻辑上的矛盾。由于规范可以使用任何 Clojure 函数，因此您可以编写一个不会终止的规范，因此无法转换为 STLC。因此 Clojure 规范并不等同于 Wadler 的主张。

有什么不同，什么相似？

正如Clojure 规范的文档所述，规范不是类型系统。规格与证明无关，但类型与证明有关。类型将我们可以编写的程序限制为那些可以静态证明“正确”的程序。类型系统具有不同级别的功能和表现力，但健全的类型系统证明了代码的某些属性。

规范并不证明您的代码的属性，而是试图让您相信您的代码可以工作，并且在不工作时让您可见。规范不能静态运行，它们从根本上讲是关于运行时值以及它们之间的关系。

但即使有这些差异，类型和 Clojure 规范也有类似的实用目的，它们都让我们对代码更有信心，它们允许我们将语义编码到函数定义中，并且都可以帮助我们生成测试，以帮助我们防止bug 会渗透到我们的代码中。