Соответствующее использование полиморфизма Вселенной

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) 

Здесь я могу продлить индуктивное определение ≈-List с дополнительным параметром уровня a, чтобы он мог принять аргумент типа типа Set a, но я неясно, как вселенные ввода и выходные отношения должны измениться. И тогда проблема выливается в более сложные определения, такие как _[_]×[_]_, где я еще менее уверен, как действовать.

Как обобщать сигнатуры в приведенном примере, так что quibble компилируется? Существуют ли общие правила, которым я могу следовать? Я читал this.

Answer 1

Я не думаю, что вы можете обобщить его на произвольные уровни юниверсов и по-прежнему иметь quibble компиляции. Произведение бинарных отношений можно обобщить достаточно легко: вы просто должны украсить Set S с одной буквой для каждого типа A через 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. Итак, вы начинаете с:

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 (так как 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 

Обратите внимание, что это имеет только одно поле типа A (который находится в Set a) и Lift A сама имеет тип Set (a ⊔ ℓ). Итак, если у вас есть x : A : Set a, вы можете перейти на более высокий уровень с помощью lift: lift a : Lift A : Set (a ⊔ ℓ) и наоборот: если у вас есть что-то в Lift A, вы можете опустить его обратно, используя ... эм .. 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) _