Idris vectors/lists

idris-vect-list.idr

data Foo : Vect m (Nat,Type) -> Vect n (Nat,Type) -> Type where
  Bar : {x:List Nat}
     -> {y:List Nat}
     -> (Vect m x -> Vect n y)
     -> Foo ?rhs1 ?rhs2

-- examples:
f : Foo [(2,Nat),(1,Nat)] [(1,Nat)]
f = Bar (\[ [x,y] , [z] ] => [ [x+y+z] ])

g : Foo [(3,Nat)] [(1,Nat),(1,Nat),(1,Nat)]
g = Bar (\[ [x,y,z] ] => [ [x] , [y] , [z] ]

{- what to be captured:

Define a type Foo with a constructor Bar that takes a function that takes
a vector of lists and returns a vector of lists, and captured in that Foo
are two parameters:

1) for each list in the input vector, a pair of the length of the list and
   the type of the elements in the list,

2) for each list in the output of the function, the same.

-}