隱長度參數在阿格達

Question

我寫一個阿格達功能prefixApp施加一個矢量函數的向量的前綴：

split : {A : Set}{m n : Nat} -> 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) 

prefixApp : {A : Set}{n m k : Nat} -> (Vec A n -> Vec A m) -> Vec A (n + k) -> Vec A (m + k) 
prefixApp f xs with split xs 
... | (ys , zs) = f ys ++ zs 

我喜歡這樣的事實，即prefixApp可以在沒有明確提供長度參數的情況下使用，例如

gate : Vec Bool 4 -> Vec Bool 3 
gate = prefixApp xorV 

（其中xorV : Vec Bool 2 -> Vec Bool 1是矢量XOR函數）

不幸的是，我不知道怎麼寫了postfixApp - 功能可以在不明確提供長度參數一起使用。我的函數的定義到目前爲止是這樣的：

postfixApp : {A : Set}{n m k : Nat} -> (Vec A n -> Vec A m) -> Vec A (k + n) -> Vec A (k + m) 
postfixApp {_} {_} {_} {k} f xs with split {_} {_} {k} xs 
... | (ys , zs) = ys ++ (f zs) 

但是它似乎，那postfixApp總是需要一個長度參數。例如。

gate : Vec Bool 4 -> Vec Bool 3 
gate = postfixApp {k = 2} xorV 

有誰知道，如何消除這種不對稱性，即如何編寫一個函數postfixApp其沒有明確的長度參數工作。我猜，我需要另一個split功能？

Answer 1

與您prefixApp，你有

prefixApp : {A : Set}{n m k : Nat} -> (Vec A n -> Vec A m) -> Vec A (n + k) -> Vec A (m + k) 

，並傳遞給它一個函數Vec Bool 2 -> Vec Bool 1，所以它知道n = 2和m = 1通過簡單的統一。然後，因爲添加由左參數遞歸定義，函數類型的其餘部分從Vec A (2 + k) -> Vec A (1 + k)減少到Vec A (suc (suc k)) -> Vec A (suc k)。然後阿格達可以應用直線上升的統一（擴大數文字量）：

Vec A (suc (suc k)) -> Vec A (suc k) 
Vec Bool (suc (suc (suc (suc zero)))) -> Vec Bool (suc (suc (suc zero))) 

推斷k = 2。

看對方一眼：

postfixApp : {A : Set}{n m k : Nat} -> (Vec A n -> Vec A m) -> Vec A (k + n) -> Vec A (k + m) 

唯一的區別是，已知量，你的xorV力量n和m爲2和1，但是這不僅使你的函數類型的剩餘部分爲Vec A (k + 2) -> Vec A (k + 1) 。此類型不會進一步減少，因爲添加是通過第一個參數k上的遞歸來定義的，該參數在此處未知。然後你試圖統一k + 2與4和k + 1與3，和Agda吐出黃色。 「但顯然k = 2，」你說！你知道，因爲你知道數學，並可以應用減法和其他簡單的原則，但Agda不知道這一點。 _+_只是它的另一個功能，統一任意函數應用程序很難。例如，如果我要求你統一(2 + x) * (2 + y)與697，例如？預計類型分析者是否應該將數字因素考慮進去並抱怨沒有獨特的因子分解？我想因爲乘法是可交換的，除非你限制雙方，否則通常不會存在，但是Agda應該知道乘法是可交換的嗎？

無論如何，Agda只知道如何做統一，基本上相互匹配「結構」數量。數據構造函數具有這種結構質量，類型構造函數也是如此，所以這些都可以毫不含糊地統一。當談到比這更奇特的事情時，你會遇到「高階統一」問題，這是一般無法解決的問題。 Agda實現了一種名爲米勒模式統一的奇特算法，它可以解決一些限制類型的更奇特的情況，但有些事情是不能做的，而你的功能應用就是其中之一。

如果你看一下標準庫，你會發現大多數情況下一個類型涉及到自然數的加法，其中一個加數（左邊的）一般不會是隱式的，除非另一個參數完全指定它（如您的prefixApp）。

至於如何處理它，通常沒有太多的問題需要解決。過了一段時間，你會發現Agda能夠推斷出什麼以及不能做什麼的感覺，然後停止讓非推斷的參數含蓄。你可以定義一個「對稱」版本的_+_，但最終雙方工作同樣痛苦，所以我也不建議這樣做。

Answer 2

實際上，可以用幾乎相同的類型來定義這個函數。

postfixApp : {A : Set}{n m k : ℕ} -> (Vec A n -> Vec A m) -> Vec A (n + k) -> Vec A (k + m) 
postfixApp f xs with splitAt' (reverse xs) 
... | ys , zs = reverse zs ++ f (reverse ys) 

test-func : Vec Bool 3 -> Vec Bool 2 
test-func (x1 ∷ x2 ∷ x3 ∷ []) = (x1 ∧ x2) ∷ (x2 ∨ x3) ∷ [] 

test : postfixApp test-func (false ∷ false ∷ true ∷ false ∷ true ∷ []) 
          ≡ false ∷ false ∷ false ∷ true ∷ [] 
test = refl 

整個代碼：http://lpaste.net/107176