haskell – 有哪些程序很好的例子很容易指定为依赖类型,但实现起来很复杂？

去年我问了“ Dependent types can prove your code is correct up to a specification. But how do you prove the specification is correct?”.投票最多的答案提出以下推理：

The hope is that your specification is simple and small enough to judge by examination,while your implementation of that might be far larger.

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

这对我来说很奇怪,因为我的问题是到处都需要依赖类型.如果你没有看到,那么以这种方式看程序.

假设我们有f :: Ord a => [a] – > [a](我将使用Haskell表示法).我们对这个函数f了解多少？换句话说,你可以预测f [],f [5,8,7],f [1,1,2,2]等应用程序？假设您知道f x = [4,6,8]那么您对x有什么看法？你可以观察到,我们知之甚少.

然后假设我告诉你f的真实名字是排序.那么关于那些相同的例子你能告诉我什么？你能告诉我关于fss = ys中xs的ys是什么意思？现在你知道了很多,但这些信息来自哪里？我所做的只是改变功能的名称;这对程序的正式含义没有意义.

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

> sort xs是xs的排列.
> sort xs是单调递增的.

我们可以使用依赖类型来证明这两个属性的排序.然后,这不仅仅是我们对分类的外在理解的问题;排序的意义成为程序的内在组成部分.

捕获bug是副作用.真正的目标是作为计划的一部分,在我们的头脑中指定和形式化我们必须知道的内容.

仔细重新考虑您已编写的程序.什么使你的程序工作的事实只在你的头脑中知道？这些都是候选人的例子.