Views in Idris - Listing 10.5 of Type-Driven Development in Idris book

Question

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

Error Message:

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

Anton Trunov Anton Trunov · Accepted Answer · 2017-05-01T17:24:46

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.

Views in Idris - Listing 10.5 of Type-Driven Development in Idris book

Error Message:

1 Answers