I am trying to feel my way into dependent types. Based on the logic of the windowl function below, I want to return a list of vectors whose length depend on the size provided.
window : (n : Nat) -> List a -> List (Vect n a)
window size = map fromList loop
where
loop xs = case splitAt size xs of
(ys, []) => if length ys == size then [ys] else []
(ys, _) => ys :: loop (drop 1 xs)
windowl : Nat -> List a -> List (List a)
windowl size = loop
where
loop xs = case List.splitAt size xs of
(ys, []) => if length ys == size then [ys] else []
(ys, _) => ys :: loop (drop 1 xs)
When I attempt to load the function into Idris, I get the following:
When checking argument func to function Prelude.Functor.map:
Type mismatch between
(l : List elem) -> Vect (length l) elem (Type of fromList)
and
a1 -> List (Vect size a) (Expected type)
Specifically:
Type mismatch between
Vect (length v0) elem
and
List (Vect size a)
When reading the documentation on fromList I notice that it says
The length of the list should be statically known.
So I assume that the type error has to do with Idris not knowing that the length of the list is corresponding to the size specified.
I am stuck because I don't even know if it is something impossible I want to do or whether I can specify that the length of the list corresponds to the length of the vector that I want to produce.
Is there a way to do that?
Since in your case it is not possible to know the length statically, we need a function which can fail at run-time:
total
fromListOfLength : (n : Nat) -> (xs : List a) -> Maybe (Vect n a)
fromListOfLength n xs with (decEq (length xs) n)
fromListOfLength n xs | (Yes prf) = rewrite (sym prf) in Just (fromList xs)
fromListOfLength n xs | (No _) = Nothing
fromListOfLength converts a list of length n into a vector of length n or fails. Now let's combine it and windowl to get to window.
total
window : (n : Nat) -> List a -> List (Vect n a)
window n = catMaybes . map (fromListOfLength n) . windowl n
Observe that the window function's type is still an underspecification of what we are doing with the input list, because nothing prevents us from always returning the empty list (this could happen if fromListOfLength returned Nothing all the time).