유니버스 레벨

유니버스 레벨 (Universe Levels)

Agda의 타입 시스템은 무한한 유니버스 계층 Setᵢ : Setᵢ₊₁을 포함해요. 이 계층은 Set : Set에서 따르는 불일치를 만나지 않고 임의의 타입에 대한 양화를 가능하게 해요. 이 유니버스들은 Agda의 sort 시스템 페이지에서 더 자세히 설명돼요.

하지만 이 계층으로 작업할 때 서로 다른 유니버스 레벨에서 같은 정의를 반복하는 것이 금방 지루해질 수 있어요. 예를 들어 data List (A : Set) : Set, data List₁ (A : Set₁) : Set₁ 같은 새 데이터 타입을 정의해야 할 수도 있어요. 또한 리스트의 모든 함수(예: append)는 모든 가능한 레벨에 대해 재정의되어야 하고, 그런 함수에 대한 모든 정리는 재증명되어야 해요.

이 문제의 해결책은 유니버스 다형성(universe polymorphism)이에요. Agda는 특수 프리미티브 타입 Level을 제공하는데, 그 원소는 유니버스의 가능한 레벨이에요. 실제로 n 번째 유니버스에 대한 표기 Setₙ은 Set n의 축약형일 뿐이며, 여기서 n : Level은 레벨이에요. 이를 사용해 어떤 레벨에서든 동작하는 다형적 List 연산자를 작성할 수 있어요. Level 타입에 접근하려면 라이브러리 Agda.Primitive를 임포트해야 해요. 정의는 다음과 같아요:

open import Agda.Primitive

data List {n : Level} (A : Set n) : Set n where
  []   : List A
  _::_ : A → List A → List A

이 새 연산자는 모든 레벨에서 동작해요. 예를 들어:

List Nat : Set
List Set : Set₁
List Set₁ : Set₂

레벨 산술 (Level arithmetic)

레벨의 수가 지정되지는 않았지만, 가장 낮은 레벨 lzero가 있고 각 레벨 n에 대해 더 높은 레벨 lsuc n이 존재한다는 것을 압니다. 따라서 레벨 집합은 무한해요. 게다가 두 레벨의 최소 상한 n ⊔ m도 취할 수 있어요. 요약하면, 레벨에 대해 다음(그리고 오직 다음) 연산들이 제공돼요:

lzero : Level
lsuc  : (n : Level) → Level
_⊔_   : (n m : Level) → Level

이것은 대부분의 목적에 충분해요. 예를 들어 임의의(반드시 같지 않은) 레벨의 두 타입의 데카르트 곱을 다음과 같이 정의할 수 있어요:

data _×_ {n m : Level} (A : Set n) (B : Set m) : Set (n ⊔ m) where
   _,_ : A → B → A × B

이 정의로 다음을 얻을 수 있어요:

Nat × Nat : Set
Nat x Set : Set₁
Set × Set : Set₁

내재 레벨 속성 (Intrinsic level properties)

레벨과 그 연산에는 컴파일러가 내부적으로 자동 해결하는 몇 가지 속성이 있어요. 이는 대응하는 레벨의 표현식이 정확히 일치하는지 걱정하지 않고 어떤 표현식을 다른 것으로 대체할 수 있게 해준다는 뜻이에요.

예를 들어 다음과 같이 쓸 수 있어요:

_ : {F : (l : Level) → Set l} {l1 l2 : Level} → F (l1 ⊔ l2) → F (l2 ⊔ l1)
_ = λ x → x

그리고 Agda는 F (l1 ⊔ l2)에서 F (l2 ⊔ l1)로의 변환을 자동으로 해요.

다음은 레벨 속성 목록이에요:

• 멱등성(Idempotence): a ⊔ a는 a와 같음
• 결합성(Associativity): (a ⊔ b) ⊔ c는 a ⊔ (b ⊔ c)와 같음
• 교환성(Commutativity): a ⊔ b는 b ⊔ a와 같음
• ⊔에 대한 lsuc의 분배성(Distributivity): lsuc (a ⊔ b)는 lsuc a ⊔ lsuc b와 같음
• lzero의 중립성(Neutrality): a ⊔ lzero는 a와 같음
• 포괄성(Subsumption): a ⊔ lsuc a는 lsuc a와 같음. 특히 이것은 임의로 많은 lsuc 사용에도 성립해요: a ⊔ lsuc (lsuc a)도 lsuc (lsuc a)와 같아요.

forall 표기 (forall notation)

Set n을 쓴다는 사실로부터 n이 레벨임을 항상 추론할 수 있어요. 따라서 유니버스-다형성 함수를 정의할 때는 ∀(또는 forall) 표기를 쓰는 것이 일반적이에요. 예를 들어 리스트의 유니버스-다형성 map 연산자의 타입은 다음과 같이 쓸 수 있어요:

map : ∀ {n m} {A : Set n} {B : Set m} → (A → B) → List A → List B

이는 다음과 동등해요:

map : {n m : Level} {A : Set n} {B : Set m} → (A → B) → List A → List B

sort Setω의 표현식 (Expressions of sort Setω)

어떤 의미에서 유니버스는 Set, Set₁ 같은 표현식을 포함한 모든 Agda 표현식이 타입을 갖도록 보장하기 위해 도입됐어요. 하지만 유니버스 다형성의 도입은 타입이 없는 몇 가지 새 항을 만들어내어 이 속성을 필연적으로 다시 깨뜨려요. 다형적 단일 원소 집합 Unit n : Setₙ을 생각해 봐요:

data Unit (n : Level) : Set n where
  <> : Unit n

이것은 잘 타입되어 있으며 다음 타입을 가져요:

Unit : (n : Level) → Set n

하지만 유효한 Agda 표현식인 타입 (n : Level) → Set n은 Set 계층의 어떤 유니버스에도 속하지 않아요. 실제로 이 표현식은 레벨을 정렬(sort)로 매핑하는 함수를 나타내므로, 타입이 있다면 Level → Sort 같은 것이어야 하고, 여기서 Sort는 모든 정렬의 모음이에요. 하지만 Agda가 모든 정렬의 정렬 Sort를 지원한다면 그것은 그 자체로 정렬이므로 특히 Sort : Sort를 갖게 돼요. Type : Type처럼 이것은 순환성과 불일치로 이어져요.

대신 Agda는 모든 sort Set ℓ 위에 서 있지만 그 자체로는 계층의 일부가 아닌 새 정렬 Setω를 도입해요. 예를 들어 Agda는 표현식 (n : Level) → Set n을 Setω 타입으로 할당해요.

Setω는 그 자체로 또 다른 무한 계층 Setωᵢ : Setωᵢ₊₁의 첫 단계예요. 하지만 이 계층은 유니버스 다형성을 지원하지 않아요. 즉 ℓ : Level에 대한 sort Setω ℓ이 없어요. 이것을 허용하려면 새 유니버스 Set2ω가 필요하고, 그것은 자연스럽게 Set2ω₁ 등으로 이어질 거예요. Setωᵢ에 유니버스 다형성을 허용하지 않는 것은 그런 훨씬 더 큰 정렬의 필요를 피해요. 이것은 의도적인 설계 결정이에요.

프래그마와 옵션 (Pragmas and options)

--type-in-type 옵션은 전체 파일에 대한 유니버스 레벨 일관성 검사를 비활성화해요.

--omega-in-omega 옵션은 타이핑 규칙 Setω : Setω를 활성화해(따라서 Agda를 불일치하게 만들지만) 그 외에는 유니버스 검사를 그대로 둬요.

--level-universe 옵션은 Level이 그 자체의 유니버스 LevelUniv에 살게 하고 레벨이 레벨 그 자체가 아닌 항에 의존하는 것을 허용하지 않게 해요. 이 옵션이 꺼지면 LevelUniv은 여전히 존재하지만 Set으로 축약돼요.

참고: --cubical 옵션과 호환되지만, 이 옵션은 현재 큐빅 빌트인 파일과는 호환되지 않으며, --level-universe를 사용하는 파일에서 임포트하려 하면 오류가 발생해요.

{-# OPTIONS --level-universe #-}
open import Agda.Primitive
open import Agda.Builtin.Nat

toLevel : Nat → Level
toLevel _ = lzero

funSort Set LevelUniv is not a valid sort
when checking that the expression Nat → Level is a type

{-# NO_UNIVERSE_CHECK #-} 프래그마는 데이터 또는 레코드 타입 앞에 두어 유니버스 일관성 검사를 로컬로 비활성화할 수 있어요. 예:

{-# NO_UNIVERSE_CHECK #-}
data U : Set where
  el : Set → U

이 프래그마는 각 생성자 인자 타입의 유니버스 레벨이 데이터 타입의 유니버스 레벨보다 작거나 같다는 검사에만 적용되고, 다른 검사에는 적용되지 않아요. 버전 2.6.0에 추가됐어요.

--type-in-type와 --omega-in-omega 옵션 및 {-# NO_UNIVERSE_CHECK #-} 프래그마는 -safe와 함께 사용할 수 없어요.

더 알아보기 (Learn more)

• Agda 문서: 유니버스 레벨 원문