generic-programming - Agda中的Arity泛型编程

Question

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

Answer 1

我将以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

IE。 comp接收一个数字 n，一个函数 g : Y -> Z和一个函数 f，它们具有Aroji格式 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)

IE。 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”论文，其中描述了如何编写接收不同类型自变量的泛型泛型函数。这个想法是将类型的向量作为参数传递，并以 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)

完全依赖和Universe多态 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现在隐藏在这些嵌套依赖对的末尾，并且可以依赖 X中任何 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

至少通过了。

如果某种类型所在的Universe依赖于值，则 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。