是否有可能编程和检查Haskell中的不变量？ [英] Is it possible to program and check invariants in Haskell?

问题描述

例如，一个函数可能会返回一个有序列表，另一个函数可能会列出一个列表将被命令。
我知道定理证明存在，但我没有使用它们的经验。

我也相信智能编译器[sic！]可以利用它们来优化程序。

那么，是否可以写下不变量并使编译器检查它们？

解决方案

好的，答案是肯定的，不是。没有办法只写一个与类型分开的不变量并检查它。在Haskell的研究分支中有一个名为ESC / Haskell的实现，但是： http：// lambda-the-ultimate.org/node/1689

您有其他各种选择。首先，您可以使用断言： http：// www .haskell.org / ghc / docs / 7.0.2 / html / users_guide / assertions.html

然后用适当的标志关掉这些断言生产。

更一般地说，您可以在您的类型中编码不变量。

另外一个例子是红黑树的非常好的编码： >

When I write an algorithm I usually write down invariants in comments.

For example, one function might return an ordered list, and the other one expect that a list would be ordered.
I'm aware that theorem provers exists, but I have no experience using them.

I also believe that smart compiler [sic!] can make use of them to optimize the program.
So, is it possible to write down invariants and make compiler check them?

解决方案

Well, the answer is yes and no. There's no way to just write an invariant separate from a type and check it. There was an implementation of this in a research fork of Haskell called ESC/Haskell, however: http://lambda-the-ultimate.org/node/1689

You do have various other options. For one, you can use asserts: http://www.haskell.org/ghc/docs/7.0.2/html/users_guide/assertions.html

Then with the appropriate flag, you can turn off these asserts for production.

More generally, you can encode the invariants in your types. I was going to add more here, but dons beat me to the punchlines.

One more example is this very nice encoding of red-black trees: http://www.reddit.com/r/haskell/comments/ti5il/redblack_trees_in_haskell_using_gadts_existential/

这篇关于是否有可能编程和检查Haskell中的不变量？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！