Difference between "null elts" and "length elts == 0"

[hafizhmakmur]

So I tried to solve the Sanitization exercise is Chapter 5 and my initial solution i fromList :: Int -> [(Int, a)] -> Maybe (Sparse a) fromList dim elts = if testList dim elts then Just (SP dim elts) else Nothing where testList dim elts | dim < 0 = False | null elts = True | fst(head(elts)) < 0 = False | fst(head(elts)) < dim = testList dim (tail elts) | otherwise = False

but it failed according to Liquid Haskell. So I tried to change it to fromList :: Int -> [(Int, a)] -> Maybe (Sparse a) fromList dim elts = if testList dim elts then Just (SP dim elts) else Nothing where testList dim elts | dim < 0 = False | length elts == 0 = True | fst(head(elts)) < 0 = False | fst(head(elts)) < dim = testList dim (tail elts) | otherwise = False

And it immediately succeed. I suspect that Liquid Haskel can't recognize null so I tried to add {-@ measure null @-} but it says "cannot extract measure from Haskell function".

So why does this happen? Shoud I never use null? I still don't really understand which built-in function I can use to reason in Liquid Haskell and which is not. Which built-in function I can use measure with is still ambiguous in general.

[ranjitjhala]

Hi @hafizhmakmur,

Excellent question! (I should add this example or similar to the tutorial!) The crux of the matter is: what is the information produced by the respective terms:

null elts

and

length elts == 0

The LH "prelude" defines specifications for some functions, it says that the type of:

length :: xs:[a] -> {v:Int | 0 <= v && v = len xs}

so the guard tells LH that in that case len elts == 0

BUT the specification for null is not present in the prelude, because, we didn't add it, so LH uses the "default" unrefined specification which is:

null :: [a] -> Bool

so the information in the guard is just True (which is not enough information to validate the "sanitization" at the refinement-level.)

However there is nothing special about null -- we left it out just because there are lots of functions and we only have partial coverage. You can, either write your own specification as:

assume null :: xs:[a] -> {b:Bool | b <=> (len xs == 0)}

If you want to use the null from the Prelude OR you can write your own null e.g.

{-@ null :: xs:[a] -> {b:Bool | b <=> (len xs == 0) } @-}
null :: [a] -> Bool
null [] = True
null (_:_) = False

and if you do either of the above, then your version of testList with null should also be verified by LH.

Does that make sense?

[ranjitjhala]

Btw, the reason it says "cannot build measure from haskell function" is you can only define measure for code that you write yourself, not that which was defined outside in an imported module (because LH doesn't even have access to that code.)

[hafizhmakmur]

@ranjitjhala Thank you very much! Looks like I miss the assume function and it looks like it's exactly what I need! Is there any comprehensive list of functions that are already defined by default in Liquid Haskell. I think it'd really be helping to have it :D .