适当使用Universe多态性 [英] Appropriate use of universe polymorphism
问题描述
我已经在一个Agda项目上工作了几周,尽我所能地轻而易举地忽略了水平多态性.不幸的是(或者幸运的是)我似乎已经到达需要开始理解它的地步.
I've been working for a couple of weeks on an Agda project, glibly ignoring level polymorphism as much as I can. Unfortunately (or perhaps fortunately) I seem to have reached the point where I need to start understanding it.
直到现在,我仅在将级别变量用作Rel
的第二个参数(或REL
的第三个参数)时才使用级别变量.否则,我将省略它们,而直接使用Set
即可.现在,我有一些客户端代码可以明确量化级别a
,并尝试将某些类型的形式Set a
传递给我的现有代码,而该代码现在是多态的.在下面的示例中,quibble
代表客户端代码,而_[_]×[_]_
和≈-List
是我现有代码的典型代表,仅使用Set
.
Until now I've been using level variables only when they are needed as a second argument to Rel
(or third argument to REL
). Otherwise I have omitted them, just using Set
directly. Now I have some client code that explicitly quantifies over levels a
and tries to pass some types of the form Set a
to my existing code, which is now insufficiently polymorphic. In the example below, quibble
represents the client code, and _[_]×[_]_
and ≈-List
are typical of my existing code which just uses Set
.
module Temp where
open import Data.List
open import Data.Product
open import Level
open import Relation.Binary
-- Direct product of binary relations.
_[_]×[_]_ : {ℓ₁ ℓ₂ : Level} {A B C D : Set} → A × B → REL A C ℓ₁ → REL B D ℓ₂ → C × D → Set (ℓ₁ ⊔ ℓ₂)
(a , b) [ _R_ ]×[ _S_ ] (c , d) = a R c × b S d
-- Extend a setoid (A, ≈) to List A.
data ≈-List {ℓ : Level} {A : Set} (_≈_ : Rel A ℓ) : Rel (List A) ℓ where
[] : ≈-List _≈_ [] []
_∷_ : {x y : A} {xs ys : List A} → (x≈y : x ≈ y) → (xs≈ys : ≈-List _≈_ xs ys) → ≈-List _≈_ (x ∷ xs) (y ∷ ys)
quibble : {a ℓ : Level} {A : Set a} → Rel A ℓ → Rel (List (A × A)) ℓ
quibble _≈_ = ≈-List (λ x y → x [ _≈_ ]×[ _≈_ ] y)
在这里,我可以用一个额外的级别参数a
扩展≈-List
的归纳定义,以便它可以接受类型为Set a
的类型实参,但是我不清楚如何输入和输出关系应该改变.然后问题就会扩散到更复杂的定义中,例如_[_]×[_]_
,我什至不确定如何进行.
Here, I can extend the inductive definition of ≈-List
with an extra level parameter a
so that it can take a type argument of type Set a
, but then I'm unclear as to how the universes of the input and output relations should change. And then problem spills out to more complex definitions such as _[_]×[_]_
where I'm even less sure how to proceed.
如何在给定的示例中概括签名,以便quibble
进行编译?我有可以遵循的一般规则吗?我已阅读此.
How should I generalise the signatures in the example given, so that quibble
compiles? Are there general rules I can follow? I've read this.
推荐答案
我认为您不能将其推广到任意Universe级别,并且仍然可以编译quibble
.二进制关系的乘积可以很容易地泛化:对于每个类型A
至D
,您只需用一个字母装饰Set
:
I don't think you can generalize it to arbitrary universe levels and still have quibble
compile. The product of binary relations can be generalized quite easily: you just have to decorate Set
s with one letter for each type A
through D
:
_[_]×[_]_ : ∀ {a b c d ℓ₁ ℓ₂}
{A : Set a} {B : Set b} {C : Set c} {D : Set d} →
A × B → REL A C ℓ₁ → REL B D ℓ₂ → C × D → Set (ℓ₁ ⊔ ℓ₂)
(a , b) [ _R_ ]×[ _S_ ] (c , d) = a R c × b S d
是的,可悲的是,宇宙多态性通常需要相当数量的样板代码.无论如何,归纳≈-List
的唯一方法是允许Set a
用于A
.因此,您从以下内容开始:
Yes, sadly universe polymorphism usually requires fair amount of boilerplate code. Anyways, the only way to generalize ≈-List
is to allow Set a
for A
. So, you start with:
data ≈-List {a ℓ} {A : Set a} (_≈_ : Rel A ℓ) : Rel (List A) a where
但这是问题所在:_∷_
构造函数的类型是什么? x
(和y
,xs
,ys
)的类型为A : Set a
,x≈y
的类型为x ≈ y : Rel A ℓ = A → A → Set ℓ
.这意味着构造函数的类型应为Set (max a ℓ)
或标准库符号为Set (a ⊔ ℓ)
.
But here's the problem: what's the type of the _∷_
constructor? The type of x
(and y
, xs
, ys
) is A : Set a
, type of x≈y
is x ≈ y : Rel A ℓ = A → A → Set ℓ
. This implies that type of the constructor should be Set (max a ℓ)
, or in standard library notation Set (a ⊔ ℓ)
.
所以是的,如果我们将≈-List
推广到A : Set a
,我们必须将其类型声明为Rel (List A) (a ⊔ ℓ)
.您可以通过没有x
,y
,xs
和ys
来使其成为Rel (List A) ℓ
,但是我想这不是一个选择.那是一个死胡同:要么使用Set
s(因为zero ⊔ ℓ = ℓ
),要么更改quibble
.
So yes, if we generalize ≈-List
to work with A : Set a
, we have to declare its type as Rel (List A) (a ⊔ ℓ)
. You could make it Rel (List A) ℓ
by not having x
, y
, xs
and ys
- but I suppose that's not an option. And that's a dead end: either use Set
s (because zero ⊔ ℓ = ℓ
) or change quibble
.
quibble
可能无法挽回,但是让我给您一个提示,当您处理Universe多态性时,很高兴知道这一点.有时您有一个A : Set a
类型,而某些则需要一个Set (a ⊔ b)
类型.现在,肯定是a ≤ a ⊔ b
,因此从Set a
转到Set (a ⊔ b)
不会引起任何矛盾(通常是Set : Set
).当然,标准库为此提供了一个工具.在Level
模块中,有一个名为Lift
的数据类型,让我们看一下它的定义:
quibble
might not be salvagable, but let me give you one tip that's nice to know when you deal with universe polymorphism. Sometimes you have a type A : Set a
and something that requires type Set (a ⊔ b)
. Now, surely a ≤ a ⊔ b
, so by going from Set a
to Set (a ⊔ b)
cannot cause any contradictions (in the usual Set : Set
sense). And of course, the standard library has a tool for this. In the Level
module, there's a data type called Lift
, let's look at its definition:
record Lift {a ℓ} (A : Set a) : Set (a ⊔ ℓ) where
constructor lift
field lower : A
注意,该字段只有一个类型为A
的字段(位于Set a
中),而Lift A
本身的类型为Set (a ⊔ ℓ)
.因此,如果您有x : A : Set a
,则可以通过lift
:lift a : Lift A : Set (a ⊔ ℓ)
移至更高的层次,反之亦然:如果您在Lift A
中包含某些内容,则可以使用... erm将其降低. >:x : Lift A : Set (a ⊔ ℓ)
和lower x : A : Set a
.
Notice that is has only one field of type A
(which is in Set a
) and Lift A
itself has a type Set (a ⊔ ℓ)
. So, if you have x : A : Set a
, you can move to higher level via lift
: lift a : Lift A : Set (a ⊔ ℓ)
and vice versa: if you have something in Lift A
, you can lower it back using... erm.. lower
: x : Lift A : Set (a ⊔ ℓ)
and lower x : A : Set a
.
我对我的代码片段进行了快速搜索,并给出了以下示例:如何仅使用依赖的消除器在Vec
tor上实现安全的head
.这是向量的依存消除器(也称为归纳原理):
I did a quick search through pile of my code snippets and it came up with this example: how to implement safe head
on Vec
tors with just the dependent eliminator. Here's the dependent eliminator (also known as induction principle) for vectors:
Vec-ind : ∀ {a p} {A : Set a} (P : ∀ n → Vec A n → Set p)
(∷-case : ∀ {n} x xs → P n xs → P (suc n) (x ∷ xs))
([]-case : P 0 []) →
∀ n (v : Vec A n) → P n v
Vec-ind P ∷-case []-case ._ [] = []-case
Vec-ind P ∷-case []-case ._ (x ∷ xs)
= ∷-case x xs (Vec-ind P ∷-case []-case _ xs)
由于我们必须处理空向量,因此我们将使用类型级别函数,该函数对于非空向量返回A
,对于空向量返回⊤
:
Since we have to deal with empty vector, we'll use type level function that returns A
for non-empty vectors and ⊤
for empty ones:
Head : ∀ {a} → ℕ → Set a → Set a
Head 0 A = ⊤
Head (suc n) A = A
但这是问题所在:我们应该返回Set a
,但是返回⊤ : Set
.所以我们Lift
它:
But here's the problem: we ought to return Set a
, but ⊤ : Set
. So we Lift
it:
Head 0 A = Lift ⊤
Head (suc n) A = A
然后我们可以写:
head : ∀ {n a} {A : Set a} → Vec A (suc n) → A
head {A = A} = Vec-ind (λ n xs → Head n A) (λ x _ _ → x) (lift tt) _
这篇关于适当使用Universe多态性的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!