隐式参数并将函数应用于固定大小向量的尾部

Question

我编写了一个Agda函数applyPrefix,将固定大小的矢量函数应用于矢量大小的较长矢量的初始部分m,n并且k 可能保持隐式.这是定义和辅助函数split:

split : ? {A m n} ? Vec A (n + m) ? (Vec A n) × (Vec A m) 
split {_} {_} {zero}  xs        = ( [] , xs )
split {_} {_} {suc _} (x ? xs) with split xs 
... | ( ys , zs ) = ( (x ? ys) , zs )


applyPrefix : ? {A n m k} ? (Vec A n ? Vec A m) ? Vec A (n + k) ? Vec A (m + k)
applyPrefix f xs with split xs
... | ( ys , zs ) = f ys ++ zs

我需要一个对称函数applyPostfix,它将固定大小的向量函数应用于较长向量的尾部.

applyPostfix ? {A n m k} ? (Vec A n ? Vec A m) ? Vec A (k + n) ? Vec A (k + m)
applyPostfix {k = k} f xs with split {_} {_} {k} xs
... | ( ys , zs ) = ys ++ (f zs)

正如applyPrefix已经显示的定义,k-Argument在applyPostfix使用时不能保持隐含.例如:

change2 : {A : Set} ? Vec A 2 ? Vec A 2
change2 ( x ? y ? [] ) = (y ? x ? [] )

changeNpre : {A : Set}{n : ?} ? Vec A (2 + n) ? Vec A (2 + n)
changeNpre = applyPrefix change2

changeNpost : {A : Set}{n : ?} ? Vec A (n + 2) ? Vec A (n + 2)
changeNpost = applyPost change2 -- does not work; n has to be provided

有没有人知道一种技术,如何实现,applyPostfix以便k在使用时-argument可能保持隐含applyPostfix？

我做的是校对/编程:

lem-plus-comm : (n m : ?) ? (n + m) ? (m + n)

并在定义时使用该引理applyPostfix:

postfixApp2 : ? {A}{n m k : ?} ? (Vec A n ? Vec A m) ? Vec A (k + n) ? Vec A (k + m)
postfixApp2 {A} {n} {m} {k} f xs rewrite lem-plus-comm n k | lem-plus-comm k n |     lem-plus-comm k m | lem-plus-comm m k = reverse (drop {n = n} (reverse xs))  ++ f (reverse (take {n = n} (reverse xs)))

不幸的是,这没有帮助,因为我使用k-Parameter来调用引理:-(

任何更好的想法如何避免k明确？也许我应该在矢量上使用snoc-View？

Answer 1

你能做的就是给出postfixApp2相同的类型applyPrefix.

问题的根源是只有知道自然数n才能统一.这是因为通过第一个参数的归纳来定义.p + qp+

所以这个工作(我正在使用标准库版本的交换+):

+-comm = comm
  where
    open IsCommutativeSemiring isCommutativeSemiring
    open IsCommutativeMonoid +-isCommutativeMonoid

postfixApp2 : {A : Set} {n m k : ?}
            ? (Vec A n ? Vec A m)
            ? Vec A (n + k) ? Vec A (m + k)
postfixApp2 {A} {n} {m} {k} f xs rewrite +-comm n k | +-comm m k =
  applyPostfix {k = k} f xs

是的,我在applyPostfix这里重复使用原件,只需重写两次就可以给它一个不同的类型.

并测试:

changeNpost : {A : Set} {n : ?} ? Vec A (2 + n) ? Vec A (2 + n)
changeNpost = postfixApp2 change2

test : changeNpost (1 ? 2 ? 3 ? 4 ? []) ? 1 ? 2 ? 4 ? 3 ? []
test = refl