Haskell缺少什么来进行总体检查？

Question

一种完全(功能)语言是一种可以显示一切终止的语言。显然，有很多地方我不希望这样-抛出的异常有时很方便，web服务器不应该终止等等。但是有时，我想要一个本地的总体检查，以支持某些优化。例如，如果我有一个可证明的全函数

commutativity :: forall (n :: Nat) (m :: Nat). n + m :~: m + n
commutativity = ...

然后，由于)，GHC可以优化

gcastWith (commutativity @n @m) someExpression
  ==>
someExpression

我对交换性的证明是从O(n)运行时成本增加到免费的。所以，现在我的问题是：

在为Haskell做一个总体检查时，有哪些微妙的困难？

显然，这样的检查器是保守的，所以每当GHC不确定某物是否完全(或懒得检查)时，它就可以假定它不是.在我看来，拼凑一个不那么聪明的检查工具可能并不太困难，因为它仍然非常有用(至少，消除我所有的算术证明应该是直接的)。然而，我似乎找不到任何努力来构建这样的东西到GHC，所以很明显，我错过了一些相当大的限制。去吧，粉碎我的梦想。:)

相关但不是最近的：尼尔·米切尔，2005。

Answer 1

液体Haskell有总体检查：https://github.com/ucsd-progsys/liquidhaskell#termination-check

​

​

默认情况下，对所有递归函数执行终止检查。 使用“不终止”选项禁用检查。 液体--无终止test.hs 在递归函数中，第一个代数或整数参数应该是递减的。 列表的默认递减度量是长度和整数它的值。

(我包括了截图和后人引用。)

类似于Agda或其他具有总体检查的语言，函数的参数必须在结构上随着时间的推移变得更小，才能到达基本情况。与总体检查器相结合，可以对许多功能进行可靠的检查。LH还支持通过指示事物如何减少来帮助检查器，这可以使用不透明的抽象数据类型或FFI。这真的很实用。