Agda 中的 Arity 泛型编程
Arity-generic programming in Agda
如何在 Agda 中编写 arity-generic 函数？是否可以编写完全依赖和全域多态 arity-generic 函数？
我以n元复合函数为例
最简单的版本
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，它具有元数 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
C-c C-r 把坑缩小到λ 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 应用于类型 X 的 n 个参数。这就像我们的 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 无法推断出该向量，即使我们提供了它的长度。因此，该论文还提供了一个用于柯里化的运算符，它从一个函数生成，该函数显式接收类型向量，一个函数，该函数接收 n 个隐式参数。
这种方法有效，但它不能扩展到完整的宇宙多态函数。我们可以通过将 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)
完全依赖和 Universe 多态性 comp
关键思想是将类型向量表示为嵌套依赖对：
Sets : ∀ {n} -> (αs : Level ^ n) -> ∀ β -> Set (mono-^ (map lsuc) αs ⊔ⁿ lsuc β)
Sets {0} _ β = Set β
Sets {suc _} (α , αs) β = Σ (Set α) λ X -> X -> Sets αs β
第二种情况读起来像"there is a type X such that all other types depend on an element of 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 现在隐藏在这些嵌套依赖对的末尾并且可以依赖于任何 [=54= 的元素] 来自 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
OK，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 无法处理函数，如果某个类型所在的宇宙依赖于一个值。例如
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ₑ
code.
如何在 Agda 中编写 arity-generic 函数？是否可以编写完全依赖和全域多态 arity-generic 函数？
我以n元复合函数为例
最简单的版本
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，它具有元数 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
C-c C-r 把坑缩小到λ 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 应用于类型 X 的 n 个参数。这就像我们的 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 无法推断出该向量，即使我们提供了它的长度。因此，该论文还提供了一个用于柯里化的运算符，它从一个函数生成，该函数显式接收类型向量，一个函数，该函数接收 n 个隐式参数。
这种方法有效，但它不能扩展到完整的宇宙多态函数。我们可以通过将 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)
完全依赖和 Universe 多态性 comp
关键思想是将类型向量表示为嵌套依赖对：
Sets : ∀ {n} -> (αs : Level ^ n) -> ∀ β -> Set (mono-^ (map lsuc) αs ⊔ⁿ lsuc β)
Sets {0} _ β = Set β
Sets {suc _} (α , αs) β = Σ (Set α) λ X -> X -> Sets αs β
第二种情况读起来像"there is a type X such that all other types depend on an element of 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 现在隐藏在这些嵌套依赖对的末尾并且可以依赖于任何 [=54= 的元素] 来自 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
OK，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 无法处理函数，如果某个类型所在的宇宙依赖于一个值。例如
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ₑ
code.