Presently I am working my way through Edwin Brady's "Type-Driven Development with Idris" text. Needless to mention, the text lists code for both SplitList and splitList (cover function).However, I wonder if the cover function given in the text could be simplified to the one that I produce below - which doesn't work as intended. Could someone please let me know why my splitList doesn't work? The error message that I receive is produced further below. Many thanks.
data SplitList : List ty -> Type where
Null : SplitList [ ]
Singleton : SplitList [x]
Pair : (lhs: List ty) -> (rhs: List ty) -> SplitList (lhs ++ rhs)
splitList : (xs: List ty) -> SplitList xs
splitList [ ] = Null
splitList [x] = Singleton
splitList xs =
let
mid = div (List.length xs) 2
lhs = List.take mid xs
rhs = List.drop mid xs
in
Pair lhs rhs
Type checking ./foo.idr foo.idr:53:11: When checking right hand side of splitList with expected type SplitList xs
Type mismatch between SplitList (lhs ++ rhs) (Type of Pair lhs rhs) and SplitList xs (Expected type)
Specifically: Type mismatch between lhs ++ rhs and xs Holes: Main.splitList
The reason for this error message is that Idris does not see that xs = lhs ++ rhs, you have to convince Idris.
First of all, let's prove the above fact as a separate lemma:
total
takeDropAppend : (n : Nat) -> (xs : List ty) -> xs = List.take n xs ++ List.drop n xs
takeDropAppend Z _ = Refl
takeDropAppend (S n) [] = Refl
takeDropAppend (S n) (x :: xs) = cong $ takeDropAppend n xs
Now we can make use of it as follows:
total
splitList : (xs: List ty) -> SplitList xs
splitList [ ] = Null
splitList [x] = Singleton
splitList xs =
let
mid = divNatNZ (List.length xs) 2 SIsNotZ
in
rewrite takeDropAppend mid xs in
Pair (List.take mid xs) (List.drop mid xs)
I changed div into divNatNZ to make the function total and took a shortcut, replacing lhs and rhs with their definitions. I should have used the (more efficient) List.splitAt standard function, but it would've complicated the proof.