Split a list in with liquidhaskell

Learn
#1

I would like to split a list into two pieces of equal or nearly equal length.
I tried this but I get an error with the function splitTwo:

{-@ halfIndex :: i : [a] -> {j : Int | j == div (len i) 2} @-}
halfIndex :: [a] -> Int
halfIndex [] = 0
halfIndex x = div (length x) 2

{-@ splitTwo :: j : [a] -> {i : ([a], [a]) | (len (fst i)) + (len (snd i)) == len j} @-}
splitTwo :: [a] -> ([a], [a])
splitTwo a = splitAt (halfIndex a) a

I am only verifying that the length of the two pieces adds up to the length of the entire list.

What other verifications do you think I should do?
Maybe that the list starts with the first piece and ends with the second? And then that the union of the sublists gives the original list? And that the difference in length of the sublists is not too large? And that the length of each sublist does not differ too much from half the length of the original list?

#2

This also gives me an error (beginsWith works, splitTwo doesn’t):

--just check termination of beginsWith
{-@ beginsWith :: i : [a] -> j : [a] -> Bool @-}
beginsWith :: (Eq a) => [a] -> [a] -> Bool
beginsWith [] [] = True
beginsWith _ [] = True
beginsWith [] _ = False
beginsWith x y =
  head x == head y && beginsWith (tail x) (tail y)

-- check if original list begins with first sublist
{-@ splitTwo :: j : [a] -> {i : ([a], [a]) | beginsWith j (fst i) == True} @-}
splitTwo :: [a] -> ([a], [a])
splitTwo a = splitAt (halfIndex a) a
#3

It would be really helpful to know what error. You mean splitTwo doesn’t compile? Or it compiles and starts to run, but then throws an error?

What are you giving as the list argument?

1 Like
#4

The code works in vanilla haskell
The command cabal repl gives me an error:

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

app/Main.hs:72:1: error:
    Liquid Type Mismatch
    .
    The inferred type
      VV : ({v : [a] | (not (len a / 2 >= 0) => len v == 0)
                       && (len a / 2 >= 0 => (not (len a < len a / 2) => len v == len a / 2)
                                             && (len a < len a / 2 => len v == len a))}, [a])<\x6 VV -> {v : [a] | len v == len a - len v}>
    .
    is not a subtype of the required type
      VV : {VV : ([a], [a]) | len (fst VV) + len (snd VV) == len a}
    .
    in the context
      a : {a : [a] | len a >= 0}
    Constraint id 20
   |
72 | splitTwo a = splitAt (halfIndex a) a
   | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Failed, no modules loaded.

It works if i remove the post condition on i:

{-@ splitTwo :: j : [a] -> i : ([a], [a]) @-}

But in this way I can only check termination

#5

Thanks. Part of the reason that inferred type is so complex is because your code is convoluted [**]. (I’m not saying it’s wrong code, but it’s making the inferred predicates very hard to follow.)

For example, why a separate halfIndex [] = 0? length [] is zero; div 0 2 is zero.

I’m not well up on LiquidHaskell. (I was hoping somebody else would jump in once you showed the message.) Here’s a possible line of thought:

LiquidHaskell seems to know splitAt splits a list into two components such that the sum of their lengths comes back to the argument’s length. It also seems to know the result from length is non-negative.

But for example splitAt 3 "ab" gives ("ab", ""), splitAt (-5) "ab" gives ("", "ab"), in which there’s no component of length of the given split offset. So I think it’s trying to assure itself that div (length x) 2 gives a non-negative split shorter than the overall list.

Try some hard-coded offsets to see if LH can follow better: splitAt 1 "ab", splitAt 0 "ab".

[**] A more Haskelly/idiomatic coding

beginsWith :: (Eq a) => [a] -> [a] -> Bool
beginsWith _ [] = True                                -- base case
beginsWith (x:xs) (y:ys) | x == y = beginsWith xs ys  -- iter case
           -- the pattern match means non-empty
beginsWith _ _ = False                                -- fail case
1 Like
#6

I’ve made some progress with your first example. The problem seems to be inside splitAt (which is a Prelude function, so I’m not sure what LH might be defining for it). I can get your splitTwo rated Safe If I change it to call mySplitAt:

{-@ mySplitAt :: ix : Int -> j : [a] -> {i : ([a], [a]) | (len (fst i)) + (len (snd i)) == len j} @-}
mySplitAt :: Int -> [a] -> ([a],[a])
mySplitAt n xs           =  (take n xs, drop n xs)        -- per Report-Prelude

Note that there’s various definitions of splitAt, take, drop. I don’t know which your LH setup would be using; some of them look super-optimised – which call on unsafeTake/Drop, and which I imagine gives LH conniptions.

You might think my predicate for mySplitAt is rather circular reasoning, but if I change the == len j to < or > or <=, the definition or something that uses it gets rejected as Unsafe, so I think it’s doing the right thing.

OTOH If I take out the predicate for mySplitAt, everything that calls it is rated Unsafe. hmm Did I say I’m not well up on LH?

(I haven’t checked your beginsWith: exercise for the reader.)

2 Likes