Agda中的Arity-generic编程

Question

如何在Agda中编写arity-generic函数？是否可以编写完全依赖和Universe多态的arity-generic函数？

Answer 1

我将以n-ary合成函数为例.

最简单的版本

open import Data.Vec.N-ary

comp : ? n {? ? ?} {X : Set ?} {Y : Set ?} {Z : Set ?}
     -> (Y -> Z) -> N-ary n X Y -> N-ary n X Z
comp  0      g y = {!!}
comp (suc n) g f = {!!}

以下是模块中的N-ary定义Data.Vec.N-ary:

N-ary : ? {?? ??} (n : ?) ? Set ?? ? Set ?? ? Set (N-ary-level ?? ?? n)
N-ary zero    A B = B
N-ary (suc n) A B = A ? N-ary n A B

即comp接收一个数字n,一个函数g : Y -> Z和一个函数f,它具有arity n和结果类型Y.

在comp 0 g y = {!!}我们的情况下

Goal : Z
y    : Y
g    : Y -> Z

因此,孔可以很容易地填充g y.

在comp (suc n) g f = {!!}情况下,N-ary (suc n) X Y减少了X -> N-ary n X Y和N-ary (suc n) X Z减少了X -> N-ary n X Z.所以我们有

Goal : X -> N-ary n X Z
f    : X -> N-ary n X Y
g    : Y -> Z

Cc Cr将孔减少到? x -> {!!}现在Goal : N-ary n X Z可以填充的孔comp n g (f x).所以整个定义是

comp : ? n {? ? ?} {X : Set ?} {Y : Set ?} {Z : Set ?}
     -> (Y -> Z) -> N-ary n X Y -> N-ary n X Z
comp  0      g y = g y
comp (suc n) g f = ? x -> comp n g (f x)

即comp接收n类型的参数X,适用f于它们然后应用于g结果.

最简单的版本与依赖 g

何时g有类型(y : Y) -> Z y

comp : ? n {? ? ?} {X : Set ?} {Y : Set ?} {Z : Y -> Set ?}
     -> ((y : Y) -> Z y) -> (f : N-ary n X Y) -> {!!}
comp  0      g y = g y
comp (suc n) g f = ? x -> comp n g (f x)

洞里应该有什么？我们不能N-ary n X Z像以前一样使用,因为Z现在是一个功能.如果Z是一个函数,我们需要将它应用于具有类型的东西Y.但要获得类型的时候,唯一的方法Y是应用f到n类型的参数X.这与我们的相似,comp但仅限于类型级别:

Comp : ? n {? ? ?} {X : Set ?} {Y : Set ?}
     -> (Y -> Set ?) -> N-ary n X Y -> Set (N-ary-level ? ? n)
Comp  0      Z y = Z y
Comp (suc n) Z f = ? x -> Comp n Z (f x)

而comp随后是

comp : ? n {? ? ?} {X : Set ?} {Y : Set ?} {Z : Y -> Set ?}
     -> ((y : Y) -> Z y) -> (f : N-ary n X Y) -> Comp n Z f
comp  0      g y = g y
comp (suc n) g f = ? x -> comp n g (f x)

带有不同类型参数的版本

有一个" Arity-generic datatype-generic programming "论文,其中描述了如何编写arity-generic函数,它们接收不同类型的参数.我们的想法是将类型的向量作为参数传递,并将其折叠为以下样式N-ary:

arrTy : {n : N} ? Vec Set (suc n) ? Set
arrTy {0}     (A :: []) = A
arrTy {suc n} (A :: As) = A ? arrTy As

然而,即使我们提供其长度,Agda也无法推断出该向量.因此,本文还提供了一个currying操作符,它通过函数显式地接收一个接收n隐式参数的类型向量,一个函数.

这种方法有效,但它不能扩展到完全的Universe多态函数.我们可以通过用运算符替换Vec数据类型来避免所有这些问题_^_:

_^_ : ? {?} -> Set ? -> ? -> Set ?
A ^ 0     = Lift ?
A ^ suc n = A × A ^ n

A ^ n是同构的Vec A n.然后我们新的N-ary是

_->?_ : ? {n} -> Set ^ n -> Set -> Set
_->?_ {0}      _      B = B
_->?_ {suc _} (A , R) B = A -> R ->? B

所有类型都是Set为了简单起见.comp现在是

comp : ? n {Xs : Set ^ n} {Y Z : Set}
     -> (Y -> Z) -> (Xs ->? Y) -> Xs ->? Z
comp  0      g y = g y
comp (suc n) g f = ? x -> comp n g (f x)

还有一个依赖的版本g:

Comp : ? n {Xs : Set ^ n} {Y : Set}
     -> (Y -> Set) -> (Xs ->? Y) -> Set
Comp  0      Z y = Z y
Comp (suc n) Z f = ? x -> Comp n Z (f x)

comp : ? n {Xs : Set ^ n} {Y : Set} {Z : Y -> Set}
     -> ((y : Y) -> Z y) -> (f : Xs ->? Y) -> Comp n Z f
comp  0      g y = g y
comp (suc n) g f = ? x -> comp n g (f x)

完全依赖和宇宙多态 comp

关键思想是将类型向量表示为嵌套依赖对:

Sets : ? {n} -> (?s : Level ^ n) -> ? ? -> Set (mono-^ (map lsuc) ?s ?? lsuc ?)
Sets {0}      _       ? = Set ?
Sets {suc _} (? , ?s) ? = ? (Set ?) ? X -> X -> Sets ?s ?

第二种情况类似于"有一种类型X,所有其他类型依赖于元素X".我们的新事物N-ary是微不足道的:

Fold : ? {n} {?s : Level ^ n} {?} -> Sets ?s ? -> Set (?s ?? ?)
Fold {0}      Y      = Y
Fold {suc _} (X , F) = (x : X) -> Fold (F x)

一个例子:

postulate
  explicit-replicate : (A : Set) -> (n : ?) -> A -> Vec A n

test : Fold (Set , ? A -> ? , ? n -> A , ? _ -> Vec A n) 
test = explicit-replicate

但什么是类型Z和g现在？

comp : ? n {? ?} {?s : Level ^ n} {Xs : Sets ?s ?} {Z : {!!}}
     -> {!!} -> (f : Fold Xs) -> Comp n Z f
comp  0      g y = g y
comp (suc n) g f = ? x -> comp n g (f x)

回想一下,f以前有类型Xs ->? Y,但Y现在隐藏在这些嵌套依赖对的末尾,并且可以依赖于任何Xfrom 的元素Xs.Z以前有型Y -> Set ?,所以现在我们需要追加Set ?到Xs,让所有x内隐:

_?>?_ : ? {n} {?s : Level ^ n} {? ?}
      -> Sets ?s ? -> Set ? -> Set (?s ?? ? ? ?)
_?>?_ {0}      Y      Z = Y -> Z
_?>?_ {suc _} (_ , F) Z = ? {x} -> F x ?>? Z

好的,有Z : Xs ?>? Set ?什么类型的g？以前是(y : Y) -> Z y.我们需要再次向嵌套的依赖对添加一些东西,因为它Y现在再次被隐藏,现在只能以依赖的方式:

?? : ? {n} {?s : Level ^ n} {? ?}
   -> (Xs : Sets ?s ?) -> (Xs ?>? Set ?) -> Set (?s ?? ? ? ?)
?? {0}      Y      Z = (y : Y) -> Z y
?? {suc _} (_ , F) Z = ? {x} -> ?? (F x) Z

最后

Comp : ? n {?s : Level ^ n} {? ?} {Xs : Sets ?s ?}
     -> (Xs ?>? Set ?) -> Fold Xs -> Set (?s ?? ?)
Comp  0      Z y = Z y
Comp (suc n) Z f = ? x -> Comp n Z (f x)

comp : ? n {? ?} {?s : Level ^ n} {Xs : Sets ?s ?} {Z : Xs ?>? Set ?}
     -> ?? Xs Z -> (f : Fold Xs) -> Comp n Z f
comp  0      g y = g y
comp (suc n) g f = ? x -> comp n g (f x)

一个测试:

length : ? {?} {A : Set ?} {n} -> Vec A n -> ?
length {n = n} _ = n

explicit-replicate : (A : Set) -> (n : ?) -> A -> Vec A n
explicit-replicate _ _ x = replicate x

foo : (A : Set) -> ? -> A -> ?
foo = comp 3 length explicit-replicate

test : foo Bool 5 true ? 5
test = refl

注意参数中的依赖关系和结果类型explicit-replicate.此外,它Set位于Set?,?而且A位于Set- 这说明了宇宙多态性.

备注

AFAIK,隐式参数没有可理解的理论,所以我不知道,当第二个函数(即f)接收隐式参数时,所有这些东西将如何工作.这个测试:

foo' : ? {?} {A : Set ?} -> ? -> A -> ?
foo' = comp 2 length (? n -> replicate {n = n})

test' : foo' 5 true ? 5
test' = refl

至少通过了.

comp如果某个类型所在的Universe依赖于某个值,则无法处理函数.例如

explicit-replicate' : ? ? -> (A : Set ?) -> (n : ?) -> A -> Vec A n
explicit-replicate' _ _ _ x = replicate x

... because this would result in an invalid use of Set? ...
error : ? ? -> (A : Set ?) -> ? -> A -> ?
error = comp 4 length explicit-replicate'

但这对于Agda来说很常见,例如你不能明确地id应用于自己:

id? : ? ? -> (A : Set ?) -> A -> A
id? _ _ x = x

-- ... because this would result in an invalid use of Set? ...
error = id? _ _ id?

该代码.