clojure - Clojure 的规范与 Wadler 的主张相同吗？

Question

Wadler写了一篇令人惊叹的论文:Propositions as Types - 他在那里谈论 Howard-Curry对应，您可以根据程序类型检查程序行为。 (对于给定的语言子集)。

最近Rich Hickey已发布Clojure spec ，用于定义数据和功能规范。

这里the commentator writes :

from Wadler we have that props ≅ types, specs ≅ props -> types ergo can do static spec/contract/type checking.

我的问题是:Clojure 的规范与 Wadler 的主张相同吗？

Answer 1

定义术语

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

例如，这些是等效的:

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

P implies Q
P
therefore Q

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

缺乏对等

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

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

什么不同，什么相似？

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

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

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