隱式自變量和應用函數到固定大小的向量的尾部

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 - 參數來調用引理:-(

任何更好的想法如何避免k是明確的嗎？也許我應該使用snoc-View on Vec職責範圍？

Answer 1

你可以做的是給postfixApp2和applyPrefix相同的類型。

問題的根源在於，只有已知p，自然數n才能與p + q統一。這是因爲+是通過第一個參數的歸納定義的。

所以這一個工程（我使用+標準庫版本可交換性）：

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