haskell - 将合同设计与类型系统进行比较

Question

我最近阅读了一篇论文，比较了按合同设计与测试驱动开发。DbC 和 TDD 之间似乎有很多重叠、一些冗余和一点点协同作用。例如，有一些系统可以根据合同自动生成测试。

DbC 以何种方式与现代类型系统（例如在 haskell 或其中一种依赖类型语言中）重叠，并且在某些方面使用两者都比两者都好？

Answer 1

Ralf Hinze、Johan Jeuring 和 Andres Löh的论文Typed Contracts for Functional Programming有一个方便的表格，说明了合同在“检查”的设计范围内的位置：

                   |   static checking    |   dynamic checking
-------------------------------------------------------------------
simple properties  | static type checking | dynamic type checking
complex properties | theorem proving      | contract checking

Answer 2

似乎大多数答案都假设合同是动态检查的。请注意，在某些系统中，合同是静态检查的。在这样的系统中，您可以将合同视为可以自动检查的依赖类型的受限形式。将此与更丰富的依赖类型进行对比，这些依赖类型以交互方式检查，例如在 Coq 中。

有关Haskell 和 OCaml 合约的静态和混合检查（静态后跟动态）的论文，请参阅Dana Xu 页面上的“规范检查”部分。许的契约体系包括细化类型和依赖箭头，两者都是依赖类型。具有自动检查的受限依赖类型的早期语言包括 Pfenning 和 Xi 的DML和ATS。在 DML 中，与 Xu 的工作不同，依赖类型受到限制，从而完成了自动检查。

Answer 3

主要区别在于测试是动态且不完整的，依靠测量来证明您已经完全验证了您正在测试的任何属性，而类型和类型检查是一个正式系统，可确保所有可能的代码路径都已针对您的任何属性进行了验证在类型中说明。

对属性的测试只能接近对同一属性的类型检查提供的开箱即用的保证水平。合同增加了动态检查的基线。

Answer 4

只要您不能在类型系统本身中表达所有假设，DBC 就很有价值。简单的haskell示例：

take n [] = []
take 0 _  = []
take n (a:as) = take (n-1) as

类型将是：

take :: Int -> [a] -> [a]

然而，只有大于等于 0 的值才适用于 n。这是 DBC 可以介入的地方，例如，生成适当的快速检查属性。

（当然，在这种情况下，也很容易检查负值并修复未定义以外的结果 - 但还有更复杂的情况。）

Answer 5

我认为 DbC 和 type 的系统没有可比性。DbC 和类型系统（甚至验证系统）之间存在混淆。例如，我们可以找到比较 DbC 和 Liquid Haskell 工具或 DbC 和 QuickCheck 框架。恕我直言，这是不正确的：类型的系统以及形式证明系统仅断言一个-您：您在我们的脑海中有一些算法，并且您声明了这些算法的属性。然后你实现这些算法。类型系统和形式证明系统验证实现代码是否与声明的属性相对应。

DbC 验证的不是内部事物（实现/代码/算法），而是外部事物：代码外部事物的预期特征。它可以是环境状态、文件系统状态、数据库状态、调用者状态、确定您自己的状态、任何东西。典型的合约在运行时工作，而不是在编译时或特殊验证阶段。

DbC 的典型示例显示了如何在 HP 芯片中发现错误。这是因为 DbC 声明了外部组件的属性：芯片、其状态、转换等。如果您的应用程序遇到意外的外部世界状态，它会将这种情况报告为异常。这里的神奇之处在于：1）您在一个地方定义合约并且不要重复自己 2）可以轻松关闭合约（从编译的二进制文件中删除）。它们更接近方面恕我直言，因为它们不像子例程调用那样“线性”。

我在这里的回顾是，DbC 比类型系统更有助于避免现实世界的错误，因为大多数真正的错误是由于对外部世界/环境/框架/操作系统组件/等的行为的误解而发生的。类型和证明帮助仅有助于避免您自己的简单错误，这些错误可以通过测试或建模（在 MatLab、Mathematica 等中）找到。

简而言之：您无法在带类型系统的 HP 芯片中找到错误。当然，存在这样的错觉，即索引 monad 之类的东西是可能的，但是具有这种尝试的真实代码看起来超级复杂、不支持且不实用。但我认为可能有一些混合方案。