6

我写了一个 Agda 函数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向量异或函数在哪里）

不幸的是，我不知道如何编写一个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-function？

4

2 回答 2

8

有了你的prefixApp，你有

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

然后你给它传递一个 function ，所以它通过简单的统一Vec Bool 2 -> Vec Bool 1知道这一点。然后，因为加法是通过对左参数的递归定义的，所以函数类型的其余部分从 减少到。然后 Agda 可以应用以下的直接统一（扩展数字文字）：n = 2m = 1Vec 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，3Agda 吐出黄色。“但很明显k = 2，”你说！你知道这一点是因为你懂数学，并且可以应用减法和其他简单的原理，但 Agda 不知道这一点。_+_只是它的另一个功能，统一任意功能应用程序很难。如果我要求你(2 + x) * (2 + y)与697， 例如？是否应该期望类型检查器分解数字并抱怨没有唯一的分解？我猜因为乘法是可交换的，除非你限制边，否则一般不会，但 Agda 是否应该知道乘法是可交换的？

无论如何，所以 Agda 只知道如何进行统一，这基本上将“结构”数量相互匹配。数据构造函数和类型构造函数一样具有这种结构质量，因此它们都可以明确统一。当涉及到比这更奇特的事情时，您会遇到“高阶统一”问题，通常无法解决。Agda 实现了一种称为米勒模式统一的奇特算法，它可以解决一些受限制的奇特情况，但有些事情它无法做到，而您的函数应用程序就是其中之一。

如果您查看标准库，您会发现大多数情况下，类型涉及自然数的加法，其中一个加数（左侧）通常不会是隐式的，除非另一个参数完全指定它（如你的案例prefixApp）。

至于如何处理它，一般来说没有太多可以解决的问题。一段时间后，您对 Agda 可以推断什么和不能推断什么有了一定的了解，然后停止隐含不可推断的论点。您可以定义 的“对称”版本_+_，但最终使用它的双方同样痛苦，所以我也不建议这样做。

于 2012-10-20T02:30:59.747 回答
1

实际上，可以用几乎相同的类型来定义这个函数。

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

于 2014-07-09T13:18:44.383 回答