I am trying to learn Liquid Haskell from the book.
To test my understanding, I wanted to write a function log2
which takes an input of the form 2^n and outputs n.
I have the following code:
powers :: [Int]
powers = map (2^) [0..]
{-@ type Powers = {v:Nat | v elem powers } @-}
{-@ log2 :: Powers -> Nat @-}
log2 :: Int -> Int
log2 n
| n == 1 = 0
| otherwise = 1 + log2 (div n 2)
But some strange error occurs while executing this code, namely "Sort Error in Refinement". I am unable to understand and resolve this error.
Any help would be really appreciated.
EDIT: From the Liquid Haskell book:
A Predicate is either an atomic predicate, obtained by comparing two expressions, or, an application of a predicate function to a list of arguments...
In the Liquid Haskell logic syntax, one of the allowed predicates are: e r e
where r
is an atomic binary relation (and functions are just special kind of relations).
Also, in the tutorial, they define the Even
subtype as:
{-@ type Even = {v:Int | v mod 2 == 0 } @-}
Based on that, I thought elem
should work.
But now as @ThomasM.DuBuisson pointed out, I thought of writing my own elem'
instead, so as to avoid confusion.
elem' :: Int -> [Int] -> Bool
elem' _ [] = False
elem' e (x:xs)
| e==x = True
| otherwise = elem' e xs
Now, as far as I understand, to be able to use this elem'
as a predicate function, I need to lift it as measure. So I added the following:
{-@ measure elem' :: Int -> [Int] -> Bool @-}
Now I replaced elem
by elem'
in type definition of Powers
. But I still get the same error as the previous one.
@TomMD is referring to the notion of "reflection" which lets you convert Haskell functions (under some restrictions) into refinements, e.g. see these posts:
https://ucsd-progsys.github.io/liquidhaskell-blog/tags/reflection.html
Unfortunately haven't gotten around to updating the tutorial with this material yet.
So for example, you can describe log2/pow2 as shown here:
https://ucsd-progsys.github.io/liquidhaskell-blog/tags/reflection.html
http://goto.ucsd.edu/liquid/index.html#?demo=permalink%2F1573673688_378.hs
In particular you can write:
You can then "check" at compile time that the following are true:
However, the type checker will reject the below
Finally, you can prove the following theorem relating
log2
andpow2
The "proof" is by "induction on n", which means:
Returning to your original question, you can define
isPow2
as:and you can "test" it does the right thing by verifying that:
and finally, by giving
pow2
the refined type:Hope this helps!