Haskell缺少整体检查的内容？

 

总（功能性）语言是一切可以显示终止的语言。 显然，有很多地方我不希望这样 - 抛出异常有时很方便，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年，Neil Mitchell未破坏Haskell。

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

主页截图

默认情况下，会对所有递归函数执行终止检查。

使用无终止选项来禁用检查

液体 - 无终止test.hs

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

列表的默认递减度量是length和Integers的值。

（我包括截图和引用后人。）

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

链接地址: http://www.djcxy.com/p/43195.html

上一篇: What is Haskell missing for totality checking?

下一篇: Benefit of Erlang for collaborative real time application