7

是否有函数式语言可以在类型检查器中指定某个计算是否保证终止？或者，您可以仅在 Haskell 中执行此操作吗？

关于 Haskell，在这个答案中，张贴者说

通常的思考方式是每个 Haskell 类型都被“提升”——它包含 ⊥。也就是说，Bool对应于{⊥, True, False}而不是仅仅{True, False}。这代表了 Haskell 程序不能保证终止并且可能有异常的事实。

另一方面，这篇关于 Agda的论文指出

一个正确的 Agda 程序是一个同时通过类型检查和终止检查的程序

即，所有的 Agda 程序都会终止，而BoolAgda 中的 a 正好对应{True, False}.

例如，在 Haskell 中你可以有一个 type 的值IO a，它告诉类型检查器需要 IO 来计算有问题的值。你能有一个类型Lifted a断言有问题的计算可能不会终止吗？也就是说，您允许不终止，但在类型系统中将其分开。（显然，就像在 Agda 中一样，您只能将值分为“绝对终止”和“可能不终止”）如果不是，是否有语言可以做到这一点？

4

1 回答 1

4

你当然可以。然而，它不会是完美的。根据定义，一些终止的计算必须驻留在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 语法中。/\意味着和。现在要在 Coq 或 Agda 中证明这样的属性，我们必须编写类似

Definition out_proof : falsy = ____.
-- Read this as
--   "A proof that there exists a number n < 0 and n > 0"

对于某个数字和的____证明在哪里？现在这非常困难，因为好吧，是错误的。显然不存在小于和大于 0 的数字。nn > 00 > nfalsy

然而，如果我们允许无限递归的非终止，

 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
于 2013-10-18T18:04:34.557 回答