什么是Haskell缺少整体检查？

Question

总(功能)语言是可以显示所有内容终止的语言.显然,有很多地方我不想要这个 - 抛出异常有时很方便,Web服务器不应该终止等等.但有时候,我希望进行本地整体检查以启用某些优化.例如,如果我有一个可证明的全部功能

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

然后,由于:~:只有一个居民(Refl),GHC可以优化

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

我的可交换性证明从O(n)运行时成本到免费.那么,现在我的问题:

为Haskell制作总体检查器有哪些微妙的困难？

显然,这样的检查是保守的,所以每当GHC不确定某些东西是完全的(或者是懒得检查)时,它可能会认为它不是......在我看来,拼凑一个不是 - 可能并不太难如此智能的检查器仍然非常有用(至少它应该是直截了当地消除我所有的算术证明).然而,我似乎无法找到任何努力在GHC中构建这样的东西,所以显然我错过了一些非常大的限制.来吧,粉碎我的梦想.:)

---

相关但不是最近的:2005年尼尔米切尔解散Haskell.

Answer 1

Liquid Haskell进行了全面检查:https://github.com/ucsd-progsys/liquidhaskell#termination-check

默认情况下,对所有递归函数执行终止检查.

使用no-termination选项禁用检查

液体 - 无终止试验

在递归函数中,第一个代数或整数参数应该减少.

列表的默认递减度量是length,Integers是其值.

(我包括后人的截图和报价.)

与Agda或其他具有整体检查的语言类似,函数的参数必须在一段时间内在结构上变小以达到基本情况.结合整体检查器,可以对许多功能进行可靠的检查.LH还支持通过指示事物减少的方式来帮助检查器,您可以使用不透明的抽象数据类型或从FFI执行操作.这真的很实用.