有哪些程序很容易被指定为依赖类型,但实现起来很复杂？

Question

去年我问过" 依赖类型可以证明你的代码在规范上是正确的.但是你如何证明规范是正确的？ ".投票最多的答案提出以下推理:

希望你的规范很简单,小到足以通过检查来判断,而你的实现可能要大得多.

这种推理对我来说很有意义.Idris是测试这些概念最容易理解的语言; 然而,由于它几乎可以像Haskell一样使用,它常常让程序员在旧概念中游荡,而不知道在哪里应用依赖类型.一些现实世界的例子可以对此有所帮助,那么,在实践中发生的程序的具体例子是什么,很容易表达为类型,但实现起来很复杂？

Answer 1

这对我来说很奇怪，因为我的问题是到处都需要依赖类型。如果您没有看到这一点，请以这种方式查看程序。

假设我们有f :: Ord a => [a] -> [a]（我将使用 Haskell 符号）。我们对这个函数了解多少f？换句话说，您可以对f []、 、f [5,8,7]等应用程序进行哪些预测f [1,1,2,2]？说你知道f x = [4,6,8]那你能说什么x？正如你所观察到的，我们知之甚少。

那么假设我告诉你 的真名f是sort。那么对于这些​​相同的例子你能告诉我什么呢？你能告诉我关于inys的什么吗？现在你知道了很多，但是这些信息从哪里来呢？我所做的只是更改了函数的名称；这在程序的正式含义中没有任何意义。xsf xs = ys

所有这些新信息都来自您对排序的了解。您知道两个定义特征：

1. sort xs是 的排列xs。
2. sort xs是单调递增的。

我们可以使用依赖类型来证明 的这两个属性sort。那么，这不仅仅是我们对排序的外在理解的问题；而是我们对排序的外在理解的问题。排序的意义成为程序的固有部分。

捕获错误是一个副作用。真正的目标是明确并形式化我们头脑中无论如何都必须知道的内容，作为该计划的一部分。

仔细重新考虑您已经编写的程序。有哪些事实可以让你的程序正常运行，而这些事实只有你自己知道？这些都是候选示例。