Agda中的Arity泛型编程 [英] Arity-generic programming in Agda
问题描述
如何在Agda中编写泛型函数?是否可以编写完全依赖的和Universe多态的Arity泛型函数?
How to write arity-generic functions in Agda? Is it possible to write fully dependent and universe polymorphic arity-generic functions?
推荐答案
我将以n元合成函数为例.
I'll take an n-ary composition function as an example.
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 = {!!}
这是在Data.Vec.N-ary
模块中定义N-ary
的方式:
Here is how N-ary
is defined in the 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
即comp
接收一个数字n
,一个函数g : Y -> Z
和一个函数f
,该函数具有Arity n
和结果类型Y
.
I.e. comp
receives a number n
, a function g : Y -> Z
and a function f
, which has the arity n
and the resulting type 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
.所以我们有
In the comp (suc n) g f = {!!}
case, N-ary (suc n) X Y
reduces to X -> N-ary n X Y
and N-ary (suc n) X Z
reduces to X -> N-ary n X Z
. So we have
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)
填充.所以整个定义是
C-c C-r reduces the hole to λ x -> {!!}
, and now Goal : N-ary n X Z
, which can be filled by comp n g (f x)
. So the whole definition is
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
接收类型为X
的n
自变量,将f
应用于它们,然后将g
应用于结果.
I.e. comp
receives n
arguments of type X
, applies f
to them and then applies g
to the result.
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
一样,但仅在类型级别上:
what should be there in the hole? We can't use N-ary n X Z
as before, because Z
is a function now. If Z
is a function, we need to apply it to something, that has type Y
. But the only way to get something of type Y
is to apply f
to n
arguments of type X
. Which is just like our comp
but only at the type level:
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通用数据类型通用编程 "一文,其中描述了如何编写接收不同类型参数的泛型泛型函数.想法是将类型的向量作为参数传递,并以N-ary
的样式将其折叠起来:
A version with arguments with different types
There is the "Arity-generic datatype-generic programming" paper, that describes, among other things, how to write arity-generic functions, that receive arguments of different types. The idea is to pass a vector of types as a parameter and fold it pretty much in the style of 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
个隐式参数.
However Agda is unable to infer that vector, even if we provide its length. Hence the paper also provides an operator for currying, which makes from a function, that explicitly receives a vector of types, a function, that receives n
implicit arguments.
此方法有效,但不能扩展到完全Universe多态函数.我们可以通过将Vec
数据类型替换为_^_
运算符来避免所有这些问题:
This approach works, but it doesn't scale to fully universe polymorphic functions. We can avoid all these problems by replacing the Vec
datatype with the _^_
operator:
_^_ : ∀ {α} -> Set α -> ℕ -> Set α
A ^ 0 = Lift ⊤
A ^ suc n = A × A ^ n
A ^ n
与Vec A n
同构.然后我们的新N-ary
是
A ^ n
is isomorphic to Vec A n
. Then our new N-ary
is
_->ⁿ_ : ∀ {n} -> Set ^ n -> Set -> Set
_->ⁿ_ {0} _ B = B
_->ⁿ_ {suc _} (A , R) B = A -> R ->ⁿ B
为简单起见,所有类型都位于Set
中. comp
现在是
All types lie in Set
for simplicity. 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
的版本:
And a version with a dependent 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
关键思想是将类型的矢量表示为嵌套的依赖对:
Fully dependent and universe polymorphic comp
The key idea is to represent a vector of types as nested dependent pairs:
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
很简单:
The second case reads like "there is a type X
such that all other types depend on an element of X
". Our new N-ary
is trivial:
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
的类型是什么?
But what are the types of 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
,但是Y
现在隐藏在这些嵌套相关对的末尾,并且可以依赖Xs
中任何X
的元素. Z
以前的类型为Y -> Set γ
,因此现在我们需要将Set γ
附加到Xs
,使所有x
都隐式:
Recall that f
previously had type Xs ->ⁿ Y
, but Y
now is hidden in the end of these nested dependent pairs and can depend on an element of any X
from Xs
. Z
previously had type Y -> Set γ
, hence now we need to append Set γ
to Xs
, making all x
s implicit:
_⋯>ⁿ_ : ∀ {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
再次被隐藏,现在仅以依赖的方式进行了
OK, Z : Xs ⋯>ⁿ Set γ
, what type has g
? Previously it was (y : Y) -> Z y
. Again we need to append something to nested dependent pairs, since Y
is again hidden, only in a dependent way now:
Πⁿ : ∀ {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
中–这说明了宇宙的多态性.
Note the dependency in the arguments and the resulting type of explicit-replicate
. Besides, Set
lies in Set₁
, while ℕ
and A
lie in Set
— this illustrates universe polymorphism.
AFAIK,对于隐式参数没有可理解的理论,所以我不知道当第二个函数(即f
)接收到隐式参数时,所有这些东西将如何工作.这项测试:
AFAIK, there is no comprehensible theory for implicit arguments, so I don't know, how all this stuff will work, when the second function (i.e. f
) receives implicit arguments. This test:
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'
但是,这对于阿格达来说很常见,例如您不能对其本身应用明确的id
But it's common for Agda, e.g. you can't apply explicit id
to itself:
idₑ : ∀ α -> (A : Set α) -> A -> A
idₑ _ _ x = x
-- ... because this would result in an invalid use of Setω ...
error = idₑ _ _ idₑ
代码.
这篇关于Agda中的Arity泛型编程的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!