我将以 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
module:
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
I.e. comp
收到一个号码n
,一个函数g : Y -> Z
和一个函数f
,其数量为n
以及结果类型Y
.
In the comp 0 g y = {!!}
我们有的情况
Goal : Z
y : Y
g : Y -> Z
因此这个洞可以很容易地被填补g y
.
In the comp (suc n) g f = {!!}
case, N-ary (suc n) X Y
减少到X -> N-ary n X Y
and 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)
I.e. comp
收到n
类型参数X
, 适用f
给他们,然后应用g
到结果。
最简单的版本,带有依赖项g
When 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
to 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)
And comp
then is
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-通用数据类型-通用编程” 论文,除其他外,描述了如何编写接收不同类型参数的 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
is
_->ⁿ_ : ∀ {n} -> Set ^ n -> Set -> Set
_->ⁿ_ {0} _ B = B
_->ⁿ_ {suc _} (A , R) B = A -> R ->ⁿ B
所有类型都位于Set
为了简单起见。comp
now is
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
and g
now?
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
, but Y
now 隐藏在这些嵌套依赖对的末尾,并且可以依赖于任何X
from Xs
. Z
以前有类型Y -> Set γ
,因此现在我们需要附加Set γ
to 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)
A test:
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₁
, while ℕ
and A
lie in Set
——这说明了宇宙的多态性。
Remarks
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ₑ
The code.