为什么Haskell有底(无限递归)？

Question

除了Haskell之外还有其他语言,例如Coq,它们禁止使用底层undefined或者无限递归定义

bot :: forall a. a
bot = bot

没有底部的好处很简单:所有程序都终止.编译器保证没有无限循环,没有无限递归.

还有一个不那么明显的好处:语言的逻辑(由库里 - 霍华德对应给出)是一致的,它不能证明是矛盾的.因此,相同的语言可以编写程序和程序正确的证明.但这可能是偏离主题的.

对无限递归的保护也很简单:强制每个递归定义都有参数(这里bot没有),并强制递归调用减少其中一个参数.这里减少的是代数数据类型,被视为构造函数和值的有限树.Coq的编译器检查递减参数是否为ADT(data在Haskell中),并且递归调用是在参数的子case of树上完成的,通常是通过a ,而不是来自其他地方的其他树.

现在这种语言约束的成本:我们失去了图灵完整性(因为我们无法解决暂停问题).这意味着有终止函数,可以使用一般递归在Haskell中编码,这将被编译器拒绝.然而,在实践中,Coq库的大小表明很少需要那些奇特的功能.有人甚至知道其中一个吗？

有些情况下无限循环是有意义的:

• 用户通过在键盘上单击或键入来发出命令的交互式程序通常会永远运行.他们等待命令,处理它然后等待下一个命令.直到时间结束,或者更严重,直到用户发出quit命令.
• 同样,不是处理无限的用户命令流,而是处理无限的数据流.比如对数据库的连续查询.

这些案例非常具体,可能会被新的语言原语处理.Haskell介绍IO了跟踪不安全的交互.为什么不在函数签名中声明无限循环的可能性？或者将复杂程序拆分为DSMS,调用Haskell函数进行纯计算？

编辑

这是一个算法示例,如果我们切换到总编程,可能会澄清哪些更改.Euclid用于计算2个数字的GCD的算法,首先是简单的递归Haskell

euclid_gcd :: Int -> Int -> Int
euclid_gcd m n = if n <= 0 then m else euclid_gcd n (m `mod` n)

关于这个函数可以证明两件事:它终止了,它确实计算了m和n的GCD.在接受证明脚本的语言中,我们会给编译器一个证据(m mod n) < n,使得它推断递归在第二个参数上减少,因此终止.

在Haskell中,我怀疑我们能做到这一点,所以我们可以尝试以结构递归的形式重写这个算法,编译器可以很容易地检查.这意味着必须在某个参数的前任上进行递归调用.这里m mod n不会这样做,所以看起来我们被卡住了.但是与尾递归一样,我们可以添加新的参数.如果我们找到递归调用数量的界限,我们就完成了.绑定不必是精确的,它只需要高于实际的递归调用数.这种约束论证通常variant在文献中被称为,我个人称之为fuel.当耗尽燃料时,我们强制递归以错误值停止.在这里我们可以取两个数字中的任何一个的继承者:

euclid_gcd_term :: Int -> Int -> Int
euclid_gcd_term m n = euclid_gcd_rec m n (n+1)
  where
    euclid_gcd_rec :: Int -> Int -> Int -> Int
    euclid_gcd_rec m n fuel =
      if fuel <= 0 then 0
      else if n <= 0 then m else euclid_gcd_rec n (m `mod` n) (fuel-1)

终止证明在某种程度上泄漏到实现中,使其稍微难以阅读.并且实现对燃料参数进行了无用的计算,这可能会减慢一点,尽管在这种情况下我希望Haskell的编译器可以忽略不计.Coq有一个提取机制,可以删除这些证明和程序混合的证明部分,以生成OCaml或Haskell代码.

至于euclid_gcd我们需要证明euclid_gcd_term确实计算n和m的GCD.这包括证明Euclid的算法终止于少于n + 1步骤.

euclid_gcd_term显然更多的工作,euclid_gcd而不是有趣的.另一方面,一旦养成这种习惯,我发现在智力上有所回报,知道我算法的界限.当我找不到这样的界限时,通常意味着我不理解我的算法.这也通常意味着他们被窃听.我们不能强迫所有开发人员对所有程序使用总编程,但是Haskell中的编译选项不能按需执行吗？

Answer 1

我无法给你一个全面的答案，但过去一年我在 Agda 工作了一段时间，以下是我看到的一些整体性的缺点。

\n\n

基本上，当用 Haskell 编写程序时，我有一些信息，但我没有明确与编译器共享。如果该信息对于程序无错误地终止是必要的，那么 Agda 会强制我明确该信息。

\n\n

考虑 Haskell 的Data.Map.!运算符，它允许您通过键查找映射中的元素。如果你传递一个不在映射中的键，它会抛出异常。该算子的 Agda 对应部分不仅需要获取密钥，还需要证明该密钥在地图中。这有一些缺点：

\n\n

\n
1. 有人必须想出一种类型，让我们表达“映射m包含键k”，并证明有关该类型如何与插入和删除交互的引理。
\n
2. insert对和的定义的任何更改都delete可能会使这些引理的证明无效。
\n
3. 当我使用这张地图时，我必须明确跟踪所有成员资格证明，传递它们并保持更新。这既是语法上的负担，也是精神上的负担。
\n
4. 如果我关心性能，我需要确保所有这些证明在运行时都被删除。
\n

\n\n

或者，我可以使用MaybeorEither显式传递这些错误。通常，这是正确的做法，但当我预计会发生错误时，或者当我根本没有费尽心思证明错误是不可能发生时，它就变得不太清楚了。这种方法也不适用于交互式调试器：我可以轻松地在异常时中断，但在构建Nothing.

\n\n

我一直关注上面的错误，但同样的事情也适用于非终止。

\n\n

这并不是说所有语言都是无用的\xe2\x80\x94，正如你所说，它们有很多好处。到目前为止，我只是不会说对于所有应用程序来说这些好处明显超过这些缺点。

\n