우주 다형성의 적절한 사용

Question

나는 가능한 한 많은 수준의 다형성을 무시하고 Agda 프로젝트에서 2 주간 작업했습니다. 불행하게도 (또는 다행스럽게도) 나는 그것을 이해하기 시작할 필요가있는 지점에 도달 한 것 같습니다.

지금까지 수준 변수는 Rel (또는 세 번째 인수 인 REL)의 두 번째 인수로 필요할 때만 사용했습니다. 그렇지 않으면 나는 단지 Set을 사용하여 그들을 생략했습니다. 이제 나는 레벨 (a)을 명시 적으로 정량화하고 어떤 유형의 양식을 Set a을 현재 기존 코드에 전달하려고 시도하는 클라이언트 코드를 가지고 있습니다.이 코드는 불충분하게 다형성이 있습니다. 아래 예에서 quibble은 클라이언트 코드를 나타내며 _[_]×[_]_과 ≈-List은 기존 코드의 대표적인 코드입니다 (Set). 이 유형 Set a의 형식 인수를 취할 수 있도록 여기에

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의 유도 정의를 확장 할 수 있지만, 그때에 관해서는 불분명 해요 어떻게 입력의 우주와 산출 관계가 바뀌어야한다. 그리고 나서 문제가 더 복잡한 정의로 쏟아져 나온다. 예를 들어 _[_]×[_]_과 같이 진행 방법을 잘 모르는 경우가있다.

quibble이 컴파일되도록 주어진 예제의 서명을 어떻게 일반화해야합니까? 내가 따라야 할 일반적인 규칙이 있습니까? 나는 this을 읽었다.

Answer 1

나는 그것을 임의의 우주 수준으로 일반화 할 수 있다고 생각하지 않으며 여전히 quibble의 컴파일을 가지고 있다고 생각하지 않습니다. 이진 관계의 제품은 아주 쉽게 일반화 할 수 있습니다 : 당신은 그냥 D을 통해 각 유형 A 하나 개의 문자로 Set의 장식해야 :

_[_]×[_]_ : ∀ {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을 일반화하는 유일한 방법은 A에 Set 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 ⊔ ℓ)으로 유형을 선언해야합니다. 당신은 을 가지고 있지 않아서 , 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 

주의는 하나의 (Set a에) 유형 A의 필드와 Lift A 자체가 유형 Set (a ⊔ ℓ)을 가지고 있습니다. lift a : Lift A : Set (a ⊔ ℓ) 그 반대를 : : 그래서 당신은 x : A : Set a이있는 경우, 당신은 lift을 통해 더 높은 레벨로 이동할 수 있습니다 x : Lift A : Set (a ⊔ ℓ) 및 lower x : A : Set a : 당신이 Lift A에 뭔가가 있다면, 당신은 ... 음 ... lower을 사용하여 다시 낮출 수 있습니다.

---

나는 내 코드 조각의 더미를 통해 빠른 검색을했고, 그것은 예를 내놓았다 : 어떻게 그냥 따라 제거기와 안전 head Vec에 TORS을 구현하는 방법. 우리는 빈 벡터 처리해야하기 때문에

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을 반환해야한다.

Head 0  A = Lift ⊤ 
Head (suc n) A = A 

을 그리고 우리가 쓸 수 있습니다 : : 그래서 우리는 그것을 Lift

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