功能程序中的终止检查
是否有函数式语言可以在类型检查器中指定某个计算是否保证终止？ 或者，你可以在Haskell中做到这一点吗？
关于Haskell，在这个答案中，海报说
通常的思考方式是每个Haskell类型都被“解除” - 它包含⊥。 也就是说， Bool对应于{⊥, True, False}而不仅仅是{True, False} 。 这表示Haskell程序不保证终止并可能有例外。
另一方面，关于Agda的这篇论文指出
正确的Agda程序是通过类型检查和终止检查的程序
也就是说，所有Agda程序都将终止，Agda中的Bool完全对应于{True, False} 。
因此，例如，在Haskell中，您可以获得IO a类型的值，它告诉类型检查者需要IO来计算有问题的值。 你可以有一个类型Lifted a ，它声称有问题的计算可能不会终止？ 也就是说，您允许不终止，但将其分开在类型系统中。 （显然，和Agda一样，只能将值分隔为“绝对终止”和“可能不终止”）。如果不是，是否有语言可以这样做？
你当然可以。 但它不会是完美的。 根据定义，一些终止的计算将不得不驻留在Lifted 。 这被称为暂停问题。
在你放弃这个想法之前，这听起来并不坏。 Coq，Agda以及其他许多工具都可以通过启发式方法检查终止。
这些实际上很重要的语言就像Coq和Agda那样，你试图证明定理。 例如，假设我们有类型
Definition falsy := exists n, n > 0 / 0 > n.
-- Read this as,
-- "The type of a proof that for some number n, n > 0 and n < 0"
在Coq语法中。 / means和。 现在要在Coq或Agda中证明这样的属性，我们必须写出类似的东西
Definition out_proof : falsy = ____.
-- Read this as
-- "A proof that there exists a number n < 0 and n > 0"
其中____证明了某些数字n ， n > 0和0 > n 。 现在这非常困难，因为falsy是错误的。 显然不存在小于和大于0的数字。
但是，如果我们允许无限递归的非终结，
Definition bottom_proof : falsy = bottom_proof.
这种类型检查，但显然不一致！ 我们只是证明了一些错误！ 因此定理证明助理强制执行某种形式的终止检查，否则它们毫无价值。
如果你想要务实，你可以使用这种提升类型来基本告诉类型分析者：“退后，我知道这可能不会终止，但我可以接受”。 这对编写真实世界的东西（如说，网络服务器或任何你可能希望它“永久”运行）有帮助。
实质上，你提出的是语言上的鸿沟，一方面，你有“验证码”，你可以安全地证明事情的真相，另一方面你有“不安全的代码”，这些代码可能永远循环。 你与IO的比较是正确的。 这与Haskell对副作用的划分完全相同。
编辑：核心数据
你提到了corecursive数据，但这不是你想要的。 这个想法是，你永远循环，但你“高效地”这样做。 实质上，递归最简单的检查方法就是总是递归一个严格小于当前所拥有的术语。
Fixpoint factorial n := match n with
| 0 => 1
| S n' => n * factorial n'
使用corecursion，您的结果词必须比您的输入“更大”。
Cofixpoint stream := Cons 1 stream
这也是不允许的
Cofixpoint stream := stream
上一篇: Termination checking in functional programs
下一篇: Why were Haskell 98's standard classes made inferior to Haskell 1.3's?