How to write a log2 function in Liquid Haskell

Question

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.

`elem` is a variable, not an infix operator. Also, where is elem defined? — Thomas M. DuBuisson, Nov 11 '19 at 19:08
@JosephSible But does liquid haskell's prelude include a lifted logical version of `elem` is the real question here. — Thomas M. DuBuisson, Nov 11 '19 at 23:00
I ask because the (admittedly out-dated) "try liquid haskell" online doesn't know what `elem` is so I suspect @kishlaya would have to provide a suitable definition for liquid Haskell to use to define `Powers` and refinment type check `log2`. — Thomas M. DuBuisson, Nov 11 '19 at 23:03
@ThomasM.DuBuisson I have edited my question with the relevant details. — kishlaya, Nov 12 '19 at 05:00
I still don't see your same error. If you look [here](http://goto.ucsd.edu:8090/index.html#?demo=permalink%2F1573574681_92.hs) you see the issue is that `powers` is not reflected nor can it be trivially. — Thomas M. DuBuisson, Nov 12 '19 at 16:05
Could you please elaborate on the phrase "`powers` is not reflected"? — kishlaya, Nov 12 '19 at 17:55

score 5 · Accepted Answer · answered Nov 13 '19 at 19:59

@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:

{-@ reflect log2 @-}
log2 :: Int -> Int
log2 1 = 0
log2 n = 1 + log2 (div n 2) 

{-@ reflect pow2 @-}
{-@ pow2 :: Nat -> Nat @-}
pow2 :: Int -> Int
pow2 0 = 1
pow2 n = 2 * pow2 (n-1)

You can then "check" at compile time that the following are true:

test8 :: () -> Int
test8 _ = log2 8 === 3

test16 :: () -> Int
test16 _ = log2 16 === 4

test3 :: () -> Int
test3 _ = pow2 3 === 8

test4 :: () -> Int
test4 _ = pow2 4 === 16

However, the type checker will reject the below

test8' :: () -> Int
test8' _ = log2 8 === 5     -- type error

Finally, you can prove the following theorem relating log2 and pow2

{-@ thm_log_pow :: n:Nat -> { log2 (pow2 n) == n } @-}

The "proof" is by "induction on n", which means:

thm_log_pow :: Int -> () 
thm_log_pow 0 = ()
thm_log_pow n = thm_log_pow (n-1)

Returning to your original question, you can define isPow2 as:

{-@ reflect isEven @-}
isEven :: Int -> Bool
isEven n = n `mod` 2 == 0

{-@ reflect isPow2 @-}
isPow2 :: Int -> Bool
isPow2 1 = True
isPow2 n = isEven n && isPow2 (n `div` 2)

and you can "test" it does the right thing by verifying that:

testPow2_8 :: () -> Bool
testPow2_8 () = isPow2 8 === True 

testPow2_9 :: () -> Bool
testPow2_9 () = isPow2 9 === False

and finally, by giving pow2 the refined type:

{-@ reflect pow2 @-}
{-@ pow2 :: Nat -> {v:Nat | isPow2 v} @-}
pow2 :: Int -> Int
pow2 0 = 1
pow2 n = 2 * pow2 (n-1)

Hope this helps!

Oh my, it can be trivial reflected. I has a mistaken assumption. — Thomas M. DuBuisson, Dec 08 '19 at 20:33

How to write a log2 function in Liquid Haskell

1 Answers1

Linked