适当使用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 Sets 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 Sets (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 Vectors 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屋！