Shouldn't the type of `dropElems` use `Vec n (a [0..1])`?

[johannes-riecken]

The type of dropElems is:

dropElems
  : forall {a : Type, m n : Nat}
  . N m -> (Vec n a) [0..1] -> Vec (n - m) a

Changing the type to

dropElems
  : forall {a : Type, m n : Nat}
  . N m -> Vec n (a [0..1]) -> Vec (n - m) a

would require a bit more code in the implementation, but it seems to me like that type should be clearer and provide better synthesis and free theorems?

[dorchard]

Well either would work- the latter can be derived from the former by use of pull, e.g.,:

import Vec

dropElems'
  : forall {a : Type, m n : Nat}
  . N m -> Vec n (a [0..1]) -> Vec (n - m) a
dropElems' n vs = dropElems n (pull @(Vec n) vs)

main : Vec 3 Int
main = dropElems' (S (S Z)) (Cons [1] (Cons [2] (Cons [3] (Cons [4] (Cons [5] Nil)))))

(dually, if we had the latter, we could derive the former using push, see: https://arxiv.org/pdf/2112.14966v1)

Although I do note it looks like we have an execution bug here with this. pull is derived from the types and it looks like this might be going wrong internally.

[DeSevilla]

When I run the example code with pull @(Vec n), I get this error, which I assume is the execution bug:

Incomplete pattern match:
  cases: [(Nil, Nil),(Cons [y0] [y1], (Cons y0) (pull@Vec y1))]
  expr: Cons [1] (Cons [2] (Cons [3] (Cons [4] (Cons [5] Nil))))

I think this is the same error as in #278 . It looks like pull is trying to derive something like this:

pull@Vec : forall {a : Type, s: Semiring, k: s, n: Nat} . Vec n (a [k]) -> (Vec n a) [k]
pull@Vec Nil = Nil
pull@Vec (Cons [x] [xs]) = Cons x (pull@Vec xs)

This doesn't typecheck when written out explicitly. There are three problems: First, the return values need to be boxed to have type (Vec n a) [k]. Second, xs shouldn't have a box at its binding site, as Vec n (a [k]) has no coeffect itself. Finally, and trickiest to solve, the output of pull@Vec xs has a coeffect and needs to be unboxed before it can be put into the Cons.

Here's a working explicit definition for pull on vectors, following these three steps:

pullVec : forall {a : Type, s: Semiring, k: s, n: Nat} . Vec n (a [k]) -> (Vec n a) [k]
pullVec Nil = [Nil];
pullVec (Cons [x] xs) = let [xs'] = pullVec xs in [Cons x xs']

I have some local changes that solve this case and I think most others like it for pull. The bad [xs] binding is, as far as I can tell, quite a simple and straightforward fix; the return-value boxing is also easy to achieve, but I'm not sure if pull should really always box returns (I'm a bit hazy on the intended semantics outside of Vec/List). On the other hand, the unboxing of pull@Vec xs has required me to hack out a separate version of mkConstructorApplication with a different type signature, including embedding it in the Checker monad. Ideally this would simply replace mkConstructorApplication in its other call sites, but I have no idea if it actually could or if it's too pull-specific.

I can submit a preliminary PR with these changes once I've tested some more cases of pull, but I'd want to make sure that at least push (& ideally other builtins) are functioning before it got merged.