Length of infinite lists

[noughtmare]

It is quite common to write an infinite list and take only a finite prefix of it. However, I believe it is not possible in Liquid Haskell to specify that a list is infinite and thus it is difficult for Liquid Haskell to know how long the resulting list is even after taking the finite prefix.

An example of this was discussed recently on discourse:

{-@ take' :: xs:[a] -> {i:Int | i < len xs} -> [a] @-}
take' :: [a] -> Int -> [a]
take' _ 0 = []
take' [] _ = []
take' (h:t) s = h : take' t (s - 1)

-- work
ex1 = take' [1,2,3,4,5] 4
-- does not work
ex2 = take' l 4
    where l = take 5 (repeat 3) -- [3,3,3,3,3]

This gives an error that is difficult to read, but essentially it is saying that it can’t verify that 4 is indeed less than the length of the list l. And it infers the length of l to be if len ?a < (5 : int) then len ?a else (5 : int). But that leaves the possibility of the list being smaller than length 5 (the true branch of the if).

The problem is that Liquid Haskell does not know that repeat creates a list that has more than 5 elements. And checking the annotations in liquid-base indeed reveals there is no annotation on repeat.

Intuitively I'd want to give it an annotation like this:

repeat :: a -> { xs:[a] | forall n. len xs > n }

However, I don't think it is possible to use quantifiers like that in liquid types. An alternative is to just use the maximum Int:

repeat :: a -> { xs:[a] | len xs > 0x7FFFFFFFFFFFFFFF }

But even that needs to be assumed.

Is there a way, or should we add a way, to specify that a list is infinitely long?

[facundominguez]

Renaming repeat to repeat1 and defining:

{-@ measure infinite :: Int @-}
{-@ invariant { v:Int | v <= infinite && v+infinite = infinite } @-}

{-@ repeat1 :: a -> { v:[a] | infinite = len v } @-}
{-@ lazy repeat1 @-}
repeat1 :: a -> [a]
repeat1 x = x : repeat1 x

makes verification pass.

I'm not too acquainted with invariant though.

Update: I changed the assumed spec of repeat1 to a verified one after posting. But since repeat1 is non-terminating, I don't think Liquid Haskell can really check that the spec is sound.

Update 2: I think it is bad idea to use this invariant. See this comment.

[ramirez7]

That works!

Is there any reason for repeat in liquid-base to not have that type as well?

[facundominguez]

Is there any reason for repeat in liquid-base to not have that type as well?

@nikivazou, @ranjitjhala?

[noughtmare]

If someone is considering changing it, I would suggest also looking at similar functions like iterate, enumFrom, enumFromThen, cycle, repeat and perhaps more? Edit: although enumFrom produces a list that is only as large as the type it is enumerating.

[facundominguez]

Actually, that invariant breaks reasoning with integers. The following is accepted then:

{-@ lemma :: { 4 = 5 }
lemma :: ()
lemma = ()

I guess this could be because the SMT solver reasons that if 4 + infinite = 5 + infinite then 4 = 5.

[noughtmare]

@facundominguez couldn't you just leave out that x + infinite = infinite:

{-@ measure infinite :: Int @-}
{-@ invariant { v:Int | v <= infinite } @-}

[facundominguez]

I'm speculating that the following reasoning could still be possible:

infinite + 1 is an Int, then by the invariant infinite + 1 <= infinite, then by subtracting infinite from both sides of the inequality we get 1 <= 0.

Here's a proof.

{-@ measure infinite :: Int @-}
{-@ invariant { v:Int | v <= infinite } @-}

{-@ infinite :: { v:Int | v = infinite } @-}
{-@ lazy infinite @-}
infinite :: Int
infinite = infinite

{-@ lemma :: x:Int -> { x <= infinite } @-}
lemma :: Int -> ()
lemma _ = ()

{-@ lemma2 :: { 1 <= 0 } @-}
lemma2 :: ()
lemma2 = lemma (infinite + 1)

[nikivazou]

invariants are not checked and it is quite dangerous to have a global invariant like this. Maybe an assume :: () -> {v:Int | v <= infinite} that you can explicitly call can do what you want.

But, the truth is that Liquid Haskell is an inductive verifier and cannot do reasoning about infinite values. That is why we need the termination checker on, to ensure that infinite values do not enter the verification picture.

If you want to talk about infinite things you need to do coinductive reasoning, as here: https://nikivazou.github.io/static/Haskell22/coinduction.pdf

[facundominguez]

I just realized that in this example, reflecting take' and repeat1 and turning on ple gets the module to pass verification.

{-@ LIQUID "--ple" @-}
{-@ LIQUID "--exact-data-cons" @-}

{-@ reflect take' @-}
{-@ reflect repeat1 @-}

This is because LH can then unfold completely the calls in 4 < len (take 5 (repeat 3)), which is what it is trying to prove.

Also, proving something like len (take' (repeat1 x) n) = n doesn't seem to require coinduction:

{-@ lemmaLenTakeRepeat :: { n:Int | n >= 0 } -> x:a -> { len (take' (repeat1 x) n) = n } @-}
lemmaLenTakeRepeat :: Int -> a -> ()
lemmaLenTakeRepeat n k =
    if n <= 0
    then ()
    else lemmaLenTakeRepeat (n-1) k

And none of these require introducing infinite or invariant :sunglasses:

[ramirez7]

I've implemented the fix here!

I also added some a postcondition to take' here:

{-@ take' :: xs:[a] -> {i:Int | i >= 0 && i < len xs} -> {ys:[a] | len ys = imin (len xs, i)} @-}

I made a new imin measure so the postcondition could be very precise.

{-@ measure imin @-}
{-@ imin :: xy:(Int, Int) -> {z:Int | z = if (fst' xy) > (snd' xy) then (snd' xy) else (fst' xy)} @-}
imin :: (Int, Int) -> Int
imin (x, y) = if x > y then y else x

Very cool to see it work! Is it possible to have multi-arg measures? I just uncurried it into a tuple and that worked.

I was wondering what the type error would be if I said ex1 had length 5 instead of 4. It was..dense:

λ :r
[1 of 1] Compiling MyLib            ( MyLib.hs, interpreted )

**** LIQUID: UNSAFE ************************************************************

MyLib.hs:42:1: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : {v : [GHC.Types.Int] | v == MyLib.take' (GHC.Types.: (1 : int) (GHC.Types.: (2 : int) (GHC.Types.: (3 : int) (GHC.Types.: (4 : int) (GHC.Types.: (5 : int) GHC.Types.[]))))) (4 : int)
                                  && len v == MyLib.imin (GHC.Tuple.(,) (len (GHC.Types.: (1 : int) (GHC.Types.: (2 : int) (GHC.Types.: (3 : int) (GHC.Types.: (4 : int) (GHC.Types.: (5 : int) GHC.Types.[])))))) (4 : int))
                                  && len v >= 0}
    .
    is not a subtype of the required type
      VV : {VV : [GHC.Types.Int] | len VV == 5}
    .
    Constraint id 7
   |
42 | ex1 = take' [1,2,3,4,5] 4
   | ^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.

If you squint, you can see the part that is the "real" length of the list (I cut an issue asking about all those conses here:

len v == MyLib.imin (GHC.Tuple.(,) (len (GHC.Types.: (1 : int) (GHC.Types.: (2 : int) (GHC.Types.: (3 : int) (GHC.Types.: (4 : int) (GHC.Types.: (5 : int) GHC.Types.[])))))) (4 : int))

On paper, I can simplify this to len v == 4

len v == MyLib.imin (GHC.Tuple.(,) (len (GHC.Types.: (1 : int) (GHC.Types.: (2 : int) (GHC.Types.: (3 : int) (GHC.Types.: (4 : int) (GHC.Types.: (5 : int) GHC.Types.[])))))) (4 : int))

-- Remove clutter
len v == imin (len [1, 2, 3, 4, 5], 4)

-- Evaluate len
len v == imin (5, 4)

-- Subst imin
-- imin = if (fst' xy) > (snd' xy) then (snd' xy) else (fst' xy)
len v == if 5 > 4 then 4 else 5

-- Evaluate 5 > 4
len v == if True then 4 else 5

-- Evaluate if-then-else
len v == 4

Is there a technical reason Liquid Haskell cannot do this to provide a better error? Is one of my steps here a "leap"? This question is off-topic, so I created a new issue for it here https://github.com/ucsd-progsys/liquidhaskell/issues/2228

[facundominguez]

Is it possible to have multi-arg measures?

measures are attached to data constructors to decide when to use them in proofs. It is not clear to me how that would be extended to multiple parameters. Here's a post conveying the intuition.

The other alternatives are using inline (since it is non-recursive) or reflect+PLE as I did before.

Is there a technical reason Liquid Haskell cannot do this to provide a better error?

I'm not aware of any reasons. There are plenty of opportunities to improve LH output. The resugaring step should be not too difficult and looks like the biggest improvement. Reducing length might be more laborious.

[ranjitjhala]

Indeed - no particular technical reason : I think we’d get far if we 1.special cased the type of cons and printed it infix, 2. Omitted the int casts in the output

On Mon, Oct 2, 2023 at 7:23 AM Facundo Domínguez @.***> wrote:

Is it possible to have multi-arg measures?

measures are attached to data constructors to decide when to use them in proofs. It is not clear to me how that would be extended to multiple parameters. Here's a post https://urldefense.com/v3/__https://ucsd-progsys.github.io/liquidhaskell/blogposts/2018-02-23-measures-and-case-splitting.lhs/__;!!Mih3wA!BbIGUeAt6qx-e3ZfoKTMUYuboSncwSluu8jTqN1JyvX5dyuHHJuGsb2pwirvgJu8k4Rh7m-0lDTeWRd9PEGyI03n$ conveying the intuition.

The other alternatives are using inline (since it is non-recursive) or reflect+PLE as I did before.

Is there a technical reason Liquid Haskell cannot do this to provide a better error?

I'm not aware of any reasons. There are plenty of opportunities to improve LH output.

— Reply to this email directly, view it on GitHub https://urldefense.com/v3/__https://github.com/ucsd-progsys/liquidhaskell/issues/2218*issuecomment-1743116029__;Iw!!Mih3wA!BbIGUeAt6qx-e3ZfoKTMUYuboSncwSluu8jTqN1JyvX5dyuHHJuGsb2pwirvgJu8k4Rh7m-0lDTeWRd9POmU93xt$, or unsubscribe https://urldefense.com/v3/__https://github.com/notifications/unsubscribe-auth/AAMS4OFIWZV5UOIZXWCE3IDX5LE47AVCNFSM6AAAAAA4T3RYFKVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTONBTGEYTMMBSHE__;!!Mih3wA!BbIGUeAt6qx-e3ZfoKTMUYuboSncwSluu8jTqN1JyvX5dyuHHJuGsb2pwirvgJu8k4Rh7m-0lDTeWRd9PBsKjdy2$ . You are receiving this because you were mentioned.Message ID: @.***>

[ramirez7]

I'm not aware of any reasons. There are plenty of opportunities to improve LH output. The resugaring step should be not too difficult and looks like the biggest improvement. Reducing length might be more laborious.

Cool! I'll continue using LH for stuff and hopefully eventually try to contribute :grin:

[facundominguez]

Hm. What a shame. I continue to find unsoundness in my solutions. Here's a module that passes verification, yet it disagrees with the runtime behavior.

{-@ LIQUID "--ple" @-}
{-@ LIQUID "--exact-data-cons" @-}

{-@ lazy repeat1 @-}
{-@ reflect repeat1 @-}
repeat1 :: a -> [a]
repeat1 x = x : repeat1 x

{-@ reflect spine @-}
spine :: [a] -> [a]
spine [] = []
spine (x:xs) = spine xs

{-@ lemmaSpine :: xs:[a] -> { spine xs == [] } @-}
lemmaSpine :: [a] -> ()
lemmaSpine [] = ()
lemmaSpine (x:xs) = lemmaSpine xs

{-@ lemmaSpineRepeat :: x:a -> { spine (repeat1 x) == [] } @-}
lemmaSpineRepeat :: a -> ()
lemmaSpineRepeat x = lemmaSpine (repeat1 x)

main = return ()

I think the reason for this to pass is that lemmaSpine proves something for every list as far as LH is concerned. So why shouldn't this work with an infinite list in particular :)

[ramirez7]

I guess spine of an infinite list is _|_, so you're asking for trouble :grin:

[facundominguez]

I think Niki's is the best answer to the starting question.

I'm closing this one, but feel free to open another issue if there are more questions.