宇宙多態性的適當使用

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