haskell - Liquid Haskell 的表现力

Question

继我最近的问题之后，我一直在思考以下问题：

我们可以在 LH 中创建一些新的惊人类型，特别是表达一些非平凡的整数子集。例如：

{-@ type Nat = {v:Int | v>=0 } @-}
{-@ type grtN N = {v:Int | v>N } @-}
{-@ type Even = {v:Int | v mod 2 == 0 } @-}

但是现在我可以在 LH 中表达哪些其他重要的子集？

我可以在 LH 中创建一个仅包含 2 次方的类型吗？这是我最后一个问题的内容，似乎答案是否定的。

所以一个自然的问题是我可以表达什么样的子集（整数）？有没有很好的性格特征？

score 2 · Accepted Answer

我相信 LH会让你写出任意算术约束。但是只有线性整数算术的理论可以由后端求解器决定（通过 presburger 算术），所以一旦你开始编写非线性表达式，你就失去了求解器会真正验证你的代码的任何保证。此外，SMT 求解器仅支持一阶逻辑，因此您无法量化关系。

1 回答 1