宇宙多态性的适当使用

Question

我已经在Agda项目上工作了几个星期，尽可能多地轻易地忽略了级别多态性。不幸的是（或者幸运的是）我似乎已经达到了需要开始理解它的程度。

到目前为止，我只在需要它们作为第二个参数时才使用级别变量作为Rel（或第三个参数为REL）的第二个参数。否则我省略了它们，直接使用Set。现在我有一些客户端代码明确量化了a级别，并试图将某些类型的Set a传递给我现有的代码，现在的代码现在不够多态。在下面的示例中，quibble代表客户端代码，而_[_]×[_]_和≈-List是我现有代码的典型代码，仅使用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类型的类型参数，但后来我不清楚如何输入的宇宙和产出关系应该改变。然后问题泄漏到更复杂的定义中，例如_[_]×[_]_，在那里我不太确定如何继续。

我应该如何概括给出的例子中的签名，以便quibble编译？我可以遵循一般规则吗？我读过this。

Answer 1

我不认为你可以将它推广到任意宇宙级别，并仍然有quibble编译。二元关系的产品可以很容易地概括：你只需要通过D装饰Set s的每种类型A一个字母：

_[_]×[_]_ : ∀ {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。所以，你开始：

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 ⊔ ℓ)。

所以是的，如果我们概括≈-List与A : Set a一起工作，我们必须声明它的类型为Rel (List A) (a ⊔ ℓ)。你可以使它Rel (List A) ℓ没有x,y,xs和ys - 但我想这不是一个选项。而这是一个死胡同：要么使用Set s（因为zero ⊔ ℓ = ℓ）要么改变quibble。

---

quibble可能不是salvagable，但让我给你一个提示，很高兴知道，当你对付宇宙多态性。有时你有一个类型A : Set a和需要类型Set (a ⊔ b)的东西。现在，当然a ≤ a ⊔ b，所以从Set a到Set (a ⊔ b)从不会引起任何矛盾（在通常的Set : Set意义上）。当然，标准库有一个工具。在Level模块，有一个名为Lift数据类型，让我们来看看它的定义：

record Lift {a ℓ} (A : Set a) : Set (a ⊔ ℓ) where 
    constructor lift 
    field lower : A 

注意，是有Lift A本身所具有的类型Set (a ⊔ ℓ)A类型的只有一个字段（在Set a）和。因此，如果您有x : A : Set a，则可以通过lift：​​移动到更高级别，反之亦然：如果您有Lift A中的某些内容，则可以使用... erm .. lower：x : Lift A : Set (a ⊔ ℓ)和lower x : A : Set a将其降回。

---

我做了一堆，通过我的代码片段的快速搜索，并想出了这个例子：如何实现安全head上Vec职权范围只依赖消除。下面是相关的消除（也称为感应原理）为载体：

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非空载体和⊤式水平仪功能空的：

Head : ∀ {a} → ℕ → Set a → Set a 
Head 0  A = ⊤ 
Head (suc n) A = A 

但这里有一个问题：我们应该回到Set a，但⊤ : Set。所以我们Lift它：

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) _