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的幂的类型吗？这是我的最后一个问题，看来答案是否定的。

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

Answer 1

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