Liquid Haskell：内联递归函数导致“循环类型别名定义”错误

Question

我写了一些Haskell代码来进行序数算术，现在正在尝试使用Liquid Haskell验证某些属性。然而，我在“反映”递归函数方面遇到了麻烦。我已经在下面的“小于”函数中分离出了一个问题：

-- (Ord a n b) = a^n + b
{-@ data Ordinal [size] = Ord { a :: Ordinal, n :: Nat,  b :: Ordinal }
                        | Zero {} @-}
data Ordinal = Ord Ordinal Integer Ordinal
             | Zero
             deriving (Eq, Show)

{-@ measure size @-}
{-@ size :: Ordinal -> Nat @-}
size :: Ordinal -> Integer
size Zero = 1
size (Ord a n b) = (size a) + 1 + (size b)

{-@ inline ordLT @-}
ordLT :: Ordinal -> Ordinal -> Bool
ordLT _ Zero = False
ordLT Zero _ = True
ordLT (Ord a0 n0 b0) (Ord a1 n1 b1) =
    (ordLT a0 a1) || 
    (a0 == a1 && n0 < n1) || 
    (a0 == a1 && n0 == n1 && ordLT b0 b1)

one = (Ord Zero 1 Zero)     -- 1
w   = (Ord one 1 Zero)      -- omega
main = print w              -- Ord (Ord Zero 1 Zero) 1 Zero

仅使用上述内容执行liquid ordinals.hs会出现以下错误：

Error: Cyclic type alias definition for `Main.ordLT`
14 |     {-@ inline ordLT @-}
                     ^^^^^
The following alias definitions form a cycle:
* `Main.ordLT`

那么如何正确地反映递归函数呢？我已经阅读了liquid haskell教程，但是我无法弄清楚它的示例与其他示例有何不同。

- Alex Varga

---

我猜你不能内联递归函数。那会怎么样？ - chi

我想我不太确定"inline"（或其他编译指示符）的作用。也许有其他更适合我的选项？ - Alex Varga

README文件似乎记录了这一点，建议您可能需要使用reflect，但我还没有多少使用LH的经验。https://github.com/ucsd-progsys/liquidhaskell/blob/develop/README.md - jberryman

这是我找到的最好的资源：https://arxiv.org/pdf/1806.03541.pdf。只需确保使用`NewProofCombinators`而不是`ProofCombinators`。 - Alex Varga

Answer 1

没有更多的上下文信息，很难确定你想要做什么，但是在递归函数中确实不能使用inline： inline 允许您通过扩展编译时函数来在类型中使用函数（在创建发送到求解器的验证条件之前），因此需要可能将每个ordLT a b的出现替换为某些特定逻辑公式（这是不可能的，因为它是递归的）。

如果您需要在逻辑中使用任意的Haskell函数，可以尝试使用精化反射。您的示例使用{-@ reflect ordLT @-}和{-@ LIQUID“--exact-data-cons”@-}编译。但是，由精化反射创建的函数符号在逻辑上不会自动完全解释。有关细节，请参见本文，并且在这些幻灯片和这篇博客文章中提供了更易于理解的例子/说明。值得记住的主要观点是，反射创建的ordLT符号最初将被视为逻辑上未经解释的函数：LH只知道有关它的东西类似于a0 == a1 ==> b0 == b1 ==> ordLT a0 b0 == ordLT a1 b1 （如果在相同输入上调用它，则结果相同）。

为了在逻辑中使用ordLT进行有用的操作，您需要在范围内的值级别上调用ordLT，这将显示该特定调用的值，因为ordLT的返回类型（值级别函数）断言有关其在这些输入上的输出的逻辑级别未解释函数的某些内容。幻灯片和文献中提供了示例。希望这足以让您入门！

- Lucy Maya Menon

---

谢谢你详细的回答，彼得！我已经意识到需要使用 reflect，但仍然在努力让 LH "理解"这个函数，我相信这些资源会有所帮助。 - Alex Varga

跟进一下：如果我声明 type LT5 = {v: Ordinal | ordLT v (Ord Zero 5 Zero)}，那我怎么样才能声明像 one:: LT5 这样的东西而不出错呢？即使我证明了 ordLT one (Ord Zero 5 Zero)，但是 LH 仍然不允许这样做。 - Alex Varga

@AlexVarga 你需要确保这个事实的证明在 Liquid 类型检查定义时是在范围内的。你可能想看一下 Language.Haskell.Liquid.ProofCombinators 模块中的一些组合器，它们专门用于处理这种情况。例如，像 one = let one' = Ord Zero 1 Zero in castWithTheorem (ordLT one' $ Ord Zero 5 Zero) one' 这样的东西应该在这种情况下起作用。 - Lucy Maya Menon