Agda中固定长度向量函数中的隐式长度参数

Question

我写了一个Agda函数prefixApp,它将Vector-Function应用于向量的前缀:

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 1Vector-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通过简单的统一.然后,因为add是通过左参数的递归来定义的,所以函数类型的其余部分从Vec A (2 + k) -> Vec A (1 + k)to 减少到Vec A (suc (suc k)) -> Vec A (suc k).然后,Agda可以应用直接统一(扩展数字文字):

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).此类型不会进一步减少,因为add是由第一个参数的递归定义的k,此时此处未知.然后,您试图统一k + 2与4和k + 1与3和阿格达吐出黄色."但很明显k = 2,"你说!你知道,因为你知道数学,并且可以应用减法和其他简单的原理,但阿格达不知道这一点._+_只是它的另一个功能,统一任意函数应用程序很难.如果我问你,统一(2 + x) * (2 + y)用697,例如？是否应该预计类型检查器会对数字进行分解并抱怨没有唯一的因子分解？我猜因为乘法是可交换的,除非你限制边,否则通常不会有,但是Agda应该知道乘法是可交换的吗？

无论如何,所以Agda只知道如何进行统一,这基本上将"结构"数量相互匹配.数据构造函数对它们具有这种结构质量,类型构造函数也是如此,因此这些都可以明确地统一.当遇到比这更漂亮的东西时,你会遇到"高阶统一"问题,这个问题一般无法解决.Agda实现了一种名为米勒模式统一的奇特算法,它可以解决一些有限的各种情况,但有些事情是它无法做到的,而你的功能应用就是其中之一.

如果你查看标准库,你会发现大多数情况下类型涉及添加自然,其中一个加数(左边的)通常不会是隐式的,除非另一个参数完全指定它(就像是你的情况prefixApp).

至于如何应对,一般来说解决这个问题并不多.过了一段时间,你会对Agda可以推断出什么以及它不能推断出什么感觉产生一种感觉,然后停止隐藏无法解决的论点.你可以定义一个"对称"版本_+_,但它最终只是同样痛苦地使用它的两面,所以我也不建议这样做.