 # Split a list in with liquidhaskell

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?

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 =

-- 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
``````

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

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
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
``````

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

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 `length`s 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"`.

``````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

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