누적성
누적성 (Cumulativity)
기초 (Basics)
Agda는 버전 2.6.1부터 --cumulativity 플래그 아래에서 유니버스의 선택적 누적성(cumulativity)을 지원해요.
{-# OPTIONS --cumulativity #-}
--cumulativity 플래그가 켜지면, Agda는 i =< j일 때마다 부분 타입 규칙 Set i =< Set j를 사용해요. 예를 들어 Nat은 평소의 타입 Set에 더해 Set₁ 타입도, 나아가 임의의 i : Level에 대해 Set i 타입도 가지게 돼요.
_ : Set
_ = Nat
_ : Set₁
_ = Nat
_ : ∀ {i} → Set i
_ = Nat
누적성이 켜져 있으면 항등 함수로 더 높은 유니버스로의 리프팅(lifting)을 구현할 수 있어요.
lift : ∀ {a b} → Set a → Set (a ⊔ b)
lift x = x
사용 예시: N항 함수 (Example usage: N-ary functions)
누적성이 없는 Agda에서 유니버스 다형적 N항 함수 타입 A → A → ... → A → B를 정의하는 것은 까다로워요. 그 이유는 유니버스 레벨이 인자의 개수가 0인지에 따라 달라지기 때문이에요:
module Without-Cumulativity where
N-ary-level : Level → Level → Nat → Level
N-ary-level ℓ₁ ℓ₂ zero = ℓ₂
N-ary-level ℓ₁ ℓ₂ (suc n) = ℓ₁ ⊔ N-ary-level ℓ₁ ℓ₂ n
N-ary : ∀ {ℓ₁ ℓ₂} n → Set ℓ₁ → Set ℓ₂ → Set (N-ary-level ℓ₁ ℓ₂ n)
N-ary zero A B = B
N-ary (suc n) A B = A → N-ary n A B
반면 누적성이 있는 Agda에서는 항상 가능한 가장 높은 유니버스 레벨로 작업할 수 있어요. 이 덕분에 N항 함수의 타입을 훨씬 쉽게 정의할 수 있답니다.
module With-Cumulativity where
N-ary : Nat → Set ℓ₁ → Set ℓ₂ → Set (ℓ₁ ⊔ ℓ₂)
N-ary zero A B = B
N-ary (suc n) A B = A → N-ary n A B
curryⁿ : (Vec A n → B) → N-ary n A B
curryⁿ {n = zero} f = f []
curryⁿ {n = suc n} f = λ x → curryⁿ λ xs → f (x ∷ xs)
_$ⁿ_ : N-ary n A B → (Vec A n → B)
f $ⁿ [] = f
f $ⁿ (x ∷ xs) = f x $ⁿ xs
∀ⁿ : ∀ {A : Set ℓ₁} n → N-ary n A (Set ℓ₂) → Set (ℓ₁ ⊔ ℓ₂)
∀ⁿ zero P = P
∀ⁿ (suc n) P = ∀ x → ∀ⁿ n (P x)
제약 사항 (Limitations)
현재 누적성은 유니버스 사이의 부분 타입 관계만 활성화하고, 유니버스를 포함하는 다른 타입들 사이의 부분 타입 관계는 활성화하지 않아요. 예를 들어 List Set은 List Set₁의 부분 타입이 아니에요. Agda는 또한 유니버스 레벨을 포함하는 다른 어떤 타입에도 누적성이 없어서, List {lzero} Nat은 List {lsuc lzero} Nat의 부분 타입이 아니에요. 이러한 규칙은 미래의 Agda 버전에 추가될 수도 있어요.
제약 해결 (Constraint solving)
누적성이 있는 Agda에서 작업할 때 유니버스 레벨 메타변수는 종종 과소 제약되어 있어요. 예를 들어 표현식 List Nat은 List {lzero} Nat을 뜻할 수도 있고, List {lsuc lzero} Nat을 뜻할 수도 있으며, 나아가 임의의 i : Level에 대해 List {i} Nat을 뜻할 수도 있어요.
현재 Agda는 유니버스 레벨 메타변수를 인스턴스화할 때 다음 휴리스틱을 사용해요. 각 타입 시그니처, 각 상호 블록(mutual block), 또는 상호 블록의 일부가 아닌 각 선언의 끝에서, Agda는 위로부터 경계가 없는(unbounded from above) 모든 유니버스 레벨 메타변수를 인스턴스화해요. 메타변수 _l : Level은 해당 메타변수를 언급하는 모든 미해결 제약이 aᵢ =< _l : Level 형태이고, _l이 다른 미해결 메타변수의 타입에 나타나지 않을 때 '위로부터 경계가 없다'고 해요. 이 조건을 만족하는 각 메타변수에 대해, _l을 언급하는 모든 제약인 a₁ =< _l : Level, …, aₙ =< _l : Level을 사용해 a₁ ⊔ a₂ ⊔ ... ⊔ aₙ으로 인스턴스화해요.
위에서 설명한 휴리스틱은 실험적인 것으로 간주되며 미래의 Agda 버전에서 바뀔 수 있어요.