I wrote some code to do ordinal arithmetic in Haskell and am now trying to use Liquid Haskell to verify certain properties. However, I'm having trouble "reflecting" recursive functions. I've isolated a problem in the "less than" function below:
-- (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
Executing liquid ordinals.hs with just the above gives the following error:
Error: Cyclic type alias definition for `Main.ordLT`
14 | {-@ inline ordLT @-}
^^^^^
The following alias definitions form a cycle:
* `Main.ordLT`
So what is the proper way to reflect recursive functions? I've read the liquid haskell tutorial but I can't figure out what its examples are doing differently.
It's a little difficult to be sure what you want to be doing without more context, but inline does indeed not work on recursive functions: inline lets you use a function in a type by expanding it at compile time (before creating the verification condition sent to the solver), so it needs to be possible to replace every occurrence of ordLT a b by some specific logic formula (which is impossible, since it's recursive).
If you need to be able to use arbitrary Haskell functions in the logic, you can look into using Refinement Reflection. Your example compiles with {-@ reflect ordLT @-} and {-@ LIQUID "--exact-data-cons" @-}. However, the function symbols created by refinement reflection are not automatically fully interpreted in the logic. The nitty-gritty details are discussed in this paper, and more approachable examples/explanation are present in these slides and this blog post. The main point to remember is that the ordLT symbol created by reflection will initially be treated as a completely uninterpreted function in the logic: the only thing that LH knows about it is something like a0 == a1 ==> b0 == b1 ==> ordLT a0 b0 == ordLT a1 b1 (if you call it on identical inputs, the results are identical).
In order to do something useful with ordLT in the logic, you will need to call ordLT at the value-level somewhere in scope, which will reveal the value of that particular call, since the return type of ordLT (the value-level function) asserts something about the output of ordLT (the logic-level uninterpreted function) on those inputs. Examples are given in the slides linked above & the paper. I hope that's enough to get you started!