List of vector slices in Idris

I am practicing Idris, and I want to obtain a list of slices from a vector.

First, I defined the following window function which returns m elements from the index i onwards (i.e. xs[i:i+m]):

import Data.Vect

window : (i : Nat) -> (m : Nat) -> Vect (i + (m + n)) t -> Vect m t
window i m xs = take m (drop i xs)

This compiles just fine:

> window 0 3 [1,2,3,4,5]
[1, 2, 3] : Vect 3 Integer

Now, for example, I want ys to hold 2 such slices of size 3, each slice beginning at i:

xs : Vect 5 Int
xs = [1,2,3,4,5]

ys : List (Vect 3 Int)
ys = [window i 3 xs | i <- [0,2]]

However, I am getting the following type mismatch:

   |
   | ys = [window i 3 xs | i <- [0,2]]
   |       ~~~~~~~~~~~~~
When checking right hand side of ys with expected type
        List (Vect 3 Int)

When checking an application of function Main.window:
        Type mismatch between
                Vect 5 Int (Type of xs)
        and
                Vect (i + (3 + n)) Int (Expected type)

        Specifically:
                Type mismatch between
                        5
                and
                        plus i (plus 3 n)

I would expect i to unify with values from [0,2], i.e.:

ys = [window 0 3 xs, window 2 3 xs]

Is my definition of window wrong?

Solution

Because of implicit parameters, the list comprehension here is not the same as writing literally

[window 0 3 xs, window 2 3 xs]

Idris' elaborator turns the above into

[window 0 3 xs {n=n1}, window 2 3 xs {n=n2}]

With open unification goals:

5 = plus 0 (plus 3 n1)
5 = plus 2 (plus 3 n2)

Because plus is recursive on the left operand it reduces:

S (S (S (S (S Z)))) = S (S (S n1)
S (S (S (S (S Z)))) = S (S (S (S (S n2))))

The unifier strips off the shared outer layers and discovers unambiguous elaborations of n for both applications.

With the comprehension, effectively you get:

ys: List (Vect 3 Int)
ys = [0,2] >>= comprehension where
  comprehension: {n: Nat} -> Nat -> List (Vect 3 t)
  comprehension i = pure (window {n} i 3 xs)

Notably, my comprehension type signature should make it clear: despite having a fixed input at the use site, comprehension is really just another case expression that must work for all possible inputs.

Idris will also not be able to infer window's n at the comprehension application: though m is fixed, i is variable. The only way around this is to use a proof-carrying structure (some type other than Vect (i+(m+n)))) or carry the size proof explicitly, which can sometimes complicate usage, but inference can still help.

Sum3: (i,m,n,s: Nat) -> Type
Sum3 i m n s = s = i + (m + n)

window: (i,m: Nat) -> Sum3 i m n s => Vect s t -> Vect m t
window i m xs = take m (drop i (replace sum3 xs {p = \l => Vect l t}))

This version of window requires the caller to provide explicit proof that the third argument's size s is equal to i + (m + n), which makes it a bit ugly for the caller:

ys: List (Vect 3 Int)                                                            
ys = [Answer.window {n} i 3 @{p} xs | (i**n**p) <- [getSum 0, getSum 2]] where    
   getSum: {n: Nat} -> (x: Nat) -> {auto sum3: Sum3 x 3 n (length Question.xs)} ->
      (i: Nat ** n: Nat ** Sum3 i 3 n (length Question.xs))                       
   getSum x = ( x ** n ** sum3 )