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

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 - 当 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 -调用引理的参数:-(

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

Answer 1

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

问题的根源在于一个自然数n可与p + q统一仅当 p是已知的。这是因为 +通过对第一个参数的归纳定义。

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

+-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