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?
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.
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
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.)