소트 시스템

소트 시스템 (Sort System)

소트(sort, 유니버스라고도 함)는 그 멤버가 다시 타입들인 타입이에요. Agda의 기본 소트는 Set이라고 불리며 작은 타입의 유니버스를 나타내요. 하지만 어떤 응용에서는 다른 소트가 필요해요. 이 페이지는 추가 소트의 필요성을 설명하고 Agda가 사용하는 모든 소트를 기술해요.

Agda 소트 시스템의 이론적 토대는 순수 타입 시스템(PTS)이에요. PTS는 지원되는 소트 집합 외에 두 개의 매개변수가 있어요:

• s : s′ 형태의 공리(axiom) 집합 — 소트 s 자체가 소트 s′를 가짐을 명시.
• (s₁, s₂, s₃) 형태의 규칙(rule) 집합 — A : s₁이고 B(x) : s₂이면 (x : A) → B(x) : s₃임을 명시.

Agda는 s₃가 s₁과 s₂에 의해 유일하게 결정된다는 의미에서 함수형 PTS예요.

공리는 내부적으로 univSort 함수로 구현돼요 (univSort 참고). 규칙은 funSort와 piSort 함수로 구현돼요 (funSort 참고).

유니버스 소개 (Introduction to universes)

러셀의 역설은 모든 집합의 모임이 그 자체로 집합이 아님을 함의해요. 즉 그러한 집합 U가 존재한다면, 자신을 포함하지 않는 모든 집합의 부분집합 A ⊆ U를 형성할 수 있어요. 그러면 A ∈ A는 A ∉ A인 경우에만 성립하게 되어 모순이 돼요.

마찬가지로 Martin-Löf 타입 이론은 원래 Set : Set 규칙을 가졌지만 Girard가 그것이 비일관적임을 보여줬어요. 이 결과는 Girard의 역설로 알려져 있어요. 따라서 모든 Agda 타입이 Set인 것은 아니에요. 예를 들어

Bool : Set
Nat  : Set

이지만 Set : Set은 아니에요. 하지만 Set이 자신만의 타입을 가지는 것이 종종 편리하므로, Agda에서는 Set에게 Set₁ 타입이 주어져요:

Set : Set₁

많은 면에서 Set₁ 타입의 표현식은 Set 타입의 표현식처럼 동작해요; 예를 들어 다른 것들의 타입으로 사용될 수 있어요. 하지만 Set₁의 원소는 잠재적으로 더 커요; A : Set₁이면 A를 때때로 큰 집합(large set)이라고 불러요. 차례로 우리는

Set₁ : Set₂
Set₂ : Set₃

를 가지며 계속돼요. 원소가 타입들인 타입을 소트 또는 유니버스라고 해요; Agda는 무한한 수의 유니버스 Set, Set₁, Set₂, Set₃, …를 제공하며, 각각은 다음 것의 원소예요. 실제로 Set 자체는 Set₀의 약어일 뿐이에요. 아래첨자 n을 유니버스 Setₙ의 레벨(level)이라고 해요.

참고: Set₁, Set₂ 대신 Set1, Set2 등으로 쓸 수도 있어요. Emacs 모드에서 아래첨자를 입력하려면 "\_1"을 입력하세요.

유니버스 예제 (Universe example)

그래서 유니버스가 왜 유용할까요? 때때로 집합뿐 아니라 큰 집합에 대해 동작하는 함수에 대한 정리를 정의하고 증명해야 하기 때문이에요. 실제로 대부분의 Agda 사용자는 조만간 Agda가 Set₁ != Set이라고 불평하는 오류 메시지를 경험해요. 이 오류들은 보통 작은 집합이 큰 집합이 기대된 곳에 사용되었거나 그 반대임을 의미해요.

예를 들어 리스트와 데카르트 곱에 대한 보통의 데이터 타입을 정의했다고 가정해 봐요:

data List (A : Set) : Set where
  [] : List A
  _::_ : A → List A → List A

data _×_ (A B : Set) : Set where
 _,_ : A → B → A × B

infixr 5 _::_
infixr 4 _,_
infixr 2 _×_

이제 n개의 집합의 리스트를 입력받아 그들의 데카르트 곱을 출력하는 연산자 Prod를 정의하고 싶다고 가정해 봐요:

Prod (A :: B :: C :: []) = A × B × C

이 정의에는 작은 문제가 하나 있어요. Prod의 타입은 다음과 같아야 해요:

Prod : List Set → Set

하지만 List A의 정의는 A가 Set이어야 하도록 지정했어요. 따라서 List Set은 유효한 타입이 아니에요. 해결책은 큰 집합에 대해 동작하는 List 연산자의 특별한 버전을 정의하는 것이에요:

data List₁ (A : Set₁) : Set₁ where
  []   : List₁ A
  _::_ : A → List₁ A → List₁ A

이것으로 우리는 실제로 다음을 정의할 수 있어요:

Prod : List₁ Set → Set
Prod []        = ⊤
Prod (A :: As) = A × Prod As

유니버스 다형성 (Universe polymorphism)

모든 가능한 유니버스 Setᵢ에 대해 동작하는 함수와 데이터 타입의 정의를 허용하기 위해 Agda는 유니버스 레벨의 타입 Level과 레벨 다형 유니버스 Set ℓ(여기서 ℓ : Level)을 제공해요. 자세한 내용은 유니버스 레벨(universe levels) 페이지를 참고하세요.

Agda의 소트 시스템 (Agda’s sort system)

Agda 소트 시스템의 구현은 순수 타입 시스템 이론에 기반해요. Agda의 전체 소트 시스템은 다음 소트들로 구성돼요:

표준 작은 소트 (유니버스 다형):

• Setᵢ와 그 유니버스 다형 변형 Set ℓ
• Propᵢ와 그 유니버스 다형 변형 Prop ℓ (--prop 포함)
• SSetᵢ와 그 유니버스 다형 변형 SSet ℓ (--two-level 포함)

표준 큰 소트 (비다형):

• Setωᵢ
• Propωᵢ (--prop 포함)
• SSetωᵢ (--two-level 포함)

특수 소트 (Special sorts):

• SizeUniv (--sized-types 포함)
• IUniv, interval universe의 약자 (--cubical 포함)
• primLockUniv (--guarded 포함)
• LevelUniv (--level-universe 포함)

작은 표준 소트 계층 Set과 Prop만 기본적으로 스코프에 있어요 (--import-sorts 참고). 그것들과 대부분의 다른 소트는 시스템 모듈 Agda.Primitive에 정의돼 있어요.

소트는 숫자 접미사의 특권을 누릴지라도, open Agda.Primitive으로 다른 Agda 정의와 똑같이 스코프로 가져와져요. 소트는 이름을 바꿀 수도 있어요. 예를 들어 open Agda.Primitive renaming (Set to Type)을 원할 수도 있어요.

일부 특수 소트는 다른 시스템 모듈에 정의돼 있어요. 특수 소트(Special sorts) 참고.

소트 Setᵢ 그리고 Set ℓ (Sorts Setᵢ and Set ℓ)

서론에서 설명했듯이 Agda에는 소트 계층 Setᵢ : Setᵢ₊₁가 있고, 여기서 i는 임의의 구체적 자연수, 즉 0, 1, 2, 3, …이에요. 소트 Set은 Set₀의 약어예요.

대안 문법 Seti로 이 소트들을 참조할 수도 있어요. 즉 Set₀, Set₁, Set₂ 대신 Set0, Set1, Set2 등을 쓸 수 있음을 의미해요.

또한 Agda는 유니버스 다형 버전 Set ℓ(여기서 ℓ : Level, 유니버스 레벨 참고)을 지원해요.

소트 Propᵢ 그리고 Prop ℓ (Sorts Propᵢ and Prop ℓ)

Setᵢ 계층 외에도 Agda는 증명-비관련 명제의 두 번째 계층 Propᵢ : Setᵢ₊₁(또는 Propi)을 지원해요. Set처럼 Prop도 유니버스 다형 버전 Prop ℓ(여기서 ℓ : Level)을 가져요.

소트 SSetᵢ 그리고 SSet ℓ (Sorts SSetᵢ and SSet ℓ)

엄격 집합(strict sets) 또는 비-fibrant 집합(non-fibrant sets)의 실험적 유니버스 SSet₀ : SSet₁ : SSet₂ : ...는 이중 레벨 타입 이론(Two-Level Type Theory)에 기술돼 있어요.

소트 Setωᵢ (Sorts Setωᵢ)

(ℓ : Level) → Set ℓ 같은 타입에 소트를 할당하기 위해 Agda는 모든 소트 Setᵢ 위에 서 있는 추가 소트 Setω를 더 지원해요.

Set과 Prop처럼 Setω는 무한 계층 Setωᵢ : Setωᵢ₊₁(여기서 Setω = Setω₀)의 가장 낮은 레벨이에요. 대안 문법 Setωi로 이 소트들을 참조할 수도 있어요. 즉 Setω₀, Setω₁, Setω₂ 대신 Setω0, Setω1, Setω2 등을 쓸 수 있어요.

하지만 표준 유니버스 계층 Setᵢ와 달리 두 번째 계층 Setωᵢ는 유니버스 다형성을 지원하지 않아요. 이것은 모든 Setωᵢ에 한 번에 양화할 수 없음을 의미해요. 예를 들어 표현식 ∀ {i} (A : Setω i) → A → A는 잘 형성된 agda 항이 아닐 거예요. 자세한 내용은 유니버스 레벨 페이지의 Setω 섹션을 참고하세요.

다른 응용에 관해서는 Agda의 정상적인 사용 중에 이 소트들을 참조할 필요는 없어야 하지만, 반영 기반 매크로를 정의하는 데 유용할 수 있어요. 그리고 Setωᵢ에서 데이터 타입을 정의하는 것은 허용돼요.

참고: --omega-in-omega가 활성화되면 Setωᵢ는 모든 i에 대해 Setω와 같다고 간주돼요 (따라서 Agda를 비일관적으로 만듦).

소트 Propωᵢ (Sorts Propωᵢ)

Prop 계층의 이 초한적(transfinite) 확장은 Setωᵢ와 유사하게 동작해요. 하지만 그것은 (ℓ : Level) → Prop ℓ을 타이핑하는 데 동기 부여되지 않는데, 그것은 Setω에 살기 때문이에요. 대신 생성자가 임의의 유한 레벨 ℓ에 사는 필드를 가질 수 있는 큰 귀납 명제를 수용하는 데 사용될 수 있어요. 유한 레벨에 대한 정렬 규칙은 초한 계층으로 확장되므로 Propωᵢ : Setωᵢ₊₁을 가져요.

소트 SSetωᵢ (Sorts SSetωᵢ)

이것은 SSet 계층의 초한적 확장이에요.

특수 소트 (Special sorts)

특수 소트는 기술적 이유로 표준 유니버스에 놓이지 않는 특수 타입을 수용해요. 보통 함수 타입 형성에 특수 법칙이 필요하기 때문이에요 (funSort 참고).

• --sized-types와 open import Agda.Builtin.Size로 특수 타입 Size와 특수 족(family) Size<를 수용하는 SizeUniv가 있어요.
• --cubical과 open import Agda.Primitive.Cubical로 구간(interval) I를 수용하는 IUniv가 있어요.
• --guarded로 primLockUniv : Set₁을 정의할 수 있는데, 여기서 Tick 타입을 postulate할 수 있어요.
• --level-universe로 Level 타입이 더 이상 Set에 살지 않고 자신만의 소트 LevelUniv에 살아요. 여전히 Agda.Primitive에 정의돼 있어요.

소트 메타변수와 알려지지 않은 소트 (Sort metavariables and unknown sorts)

유니버스 다형성 아래에서 레벨은 임의의 항이 될 수 있어요. 예를 들어 자유 변수를 포함하는 레벨. 때때로 우리는 어떤 표현식이 어떤 소트를 가지는지 모르는 채로 유효한 타입을 가짐을 확인해야 할 거예요. 이러한 이유로 Agda의 소트 내부 표현은 알려지지 않은 소트를 나타내는 생성자(소트 메타변수)를 구현해요. 제약 해결사는 일반 항 메타변수를 계산하듯 소트 메타변수를 계산할 수 있어요.

하지만 소트 메타변수의 존재는 다른 타입의 소트가 때때로 직접 계산될 수 없음을 의미하기도 해요. 이러한 이유로 Agda의 소트 내부 표현은 univSort, funSort, piSort라는 세 개의 추가 생성자를 포함해요. 이 생성자들은 인자의 충분한 메타변수가 해결되면 적절한 소트로 계산돼요.

참고: univSort, funSort, piSort는 항을 평가할 때 출력될 수 있는 내부 생성자예요. 사용자가 그것들을 입력하거나 Agda 코드에 도입할 수 없어요. 이 생성자들은 모두 새 소트를 나타내지 않고, 인자가 알려지면 올바른 소트로 계산돼요.

univSort

univSort는 주어진 소트의 후임자 소트를 반환해요. PTS 용어로는 공리 s : univSort s를 구현해요.

univSort	소트	후임자 소트
univSort	Prop a	Prop (lsuc a)
univSort	Set a	Set (lsuc a)
univSort	SSet a	SSet (lsuc a)
univSort	Propωᵢ	Propωᵢ₊₁
univSort	Setωᵢ	Setωᵢ₊₁
univSort	SSetωᵢ	SSetωᵢ₊₁
univSort	SizeUniv	Setω
univSort	IUniv	SSet₁
univSort	LockUniv	Set₁
univSort	LevelUniv	Set₁

| univSort | _1 | univSort _1 |

funSort

생성자 funSort는 정의역의 소트와 공역의 소트가 여전히 알려지지 않아도 함수 타입의 소트를 계산해요.

funSort가 일반적으로 어떻게 동작하는지 이해하기 위해 다음과 같은 시나리오를 가정해 봐요:

• sA와 sB는 두 개의 (아마 다른) 소트.
• A : sA — A가 소트 sA를 가지는 타입임을 의미.
• B : sB — B가 소트 sB를 가지는 (아마 다른) 타입임을 의미.

이 조건들 아래에서 함수 타입 A → B : funSort sA sB를 만들 수 있어요. 이 타입 시그니처는 함수 타입 A → B가 (아마 알려지지 않은) 그러나 잘 정의된 소트 funSort sA sB를 가지며, 그것의 정의역과 공역의 소트 측면에서 명시됨을 의미해요.

예제: 정규 형태 {A : _5} → A → A를 가진 함수 타입 ∀ {A} → A → A의 소트는 funSort (univSort _5) (funSort _5 _5)로 평가되는데, 여기서:

• _5는 A의 소트를 나타내는 메타변수.
• funSort _5 _5는 A → A의 소트.

sA와 sB가 우연히 알려져 있으면 funSort sA sB는 소트 값으로 계산될 수 있어요.

funSort가 어떻게 계산하는지 명시하기 위해, U가 Prop, Set, SSet에 걸쳐 있다고 하고 U ↝ U'가 U, U' 중 하나가 SSet이면 SSet, 그렇지 않으면 U'가 되게 해요. 예: SSet ↝ Prop은 SSet, Set ↝ Prop은 Prop. 또한 L이 레벨 a와 초한수 ωᵢ(즉 ω + i)에 걸쳐 있다고 하고 ⊔를 L ⊔ L'로 일반화해요. 예: a ⊔ ωᵢ = ωᵢ, ωᵢ ⊔ ωⱼ = ωₖ(여기서 k = max i j). 표준 유니버스를 쌍 U L로 씁니다. 예: Propωᵢ를 쌍 Prop ωᵢ로. S가 특수 유니버스 SizeUniv, IUniv, LockUniv, LevelUniv에 걸쳐 있다고 해요.

다음 표에서 funSort s₁ s₂가 알려진 소트 s₁과 s₂에 대해 어떻게 계산하는지 지정해요 (서로 다른 특수 소트 사이의 상호작용 제외). PTS 용어로 이것들은 규칙 (s₁, s₂, funSort s₁ s₂)예요.

funSort	s₁	s₂	funSort s₁ s₂
	U L	U' L'	(U ↝ U') (L ⊔ L')
	U L	IUniv	SSet L
	U ωᵢ	S ≠ IUniv	Set ωᵢ
	U a	SizeUniv	SizeUniv
	S	U ωᵢ	U ωᵢ
	S ≠ LevelUniv	U a	U a
	LevelUniv	U a	U a
	U ω₀	LevelUniv	U a
	LevelUniv	LevelUniv	LevelUniv
	SizeUniv	SizeUniv	SizeUniv
	IUniv	IUniv	SSet₀

표준 유니버스 U L에 대한 몇 가지 예제:

funSort Setωᵢ    Setωⱼ    = Setωₖ            (k = max(i,j)일 때)
funSort Setωᵢ    (Set b)  = Setωᵢ
funSort Setωᵢ    (Prop b) = Setωᵢ
funSort (Set a)  Setωⱼ    = Setωⱼ
funSort (Prop a) Setωⱼ    = Setωⱼ
funSort (Set a)  (Set b)  = Set (a ⊔ b)
funSort (Prop a) (Set b)  = Set (a ⊔ b)
funSort (Set a)  (Prop b) = Prop (a ⊔ b)
funSort (Prop a) (Prop b) = Prop (a ⊔ b)

참고: funSort는 인자 두 개만 받아들일 수 있으므로, 함수 타입이 여러 인자를 가지면 반복될 거예요. 예를 들어 함수 타입 ∀ {A} → A → A → A는 funSort (univSort _5) (funSort _5 (funSort _5 _5))로 평가돼요.

piSort

마찬가지로 piSort s1 (λ x → s2)는 정의역의 소트 s1과 공역의 소트 s2를 인자로 받아 Π-타입의 소트를 계산하는 funSort의 더 일반적인 버전이에요. Π-타입의 공역 소트가 Π-타입이 바인딩하는 변수에 의존할 수 있는 경우에 사용돼요. 그것은 (공역 소트가 의존하지 않으면) funSort로, (의존하면) Setω로 계산돼요.

piSort가 일반적으로 어떻게 동작하는지 이해하기 위해 다음과 같은 시나리오를 설정해요:

• sA와 sB는 두 개의 (아마 다른) 소트.
• A : sA — A가 소트 sA를 가지는 타입임을 의미.
• x : A — x가 타입 A를 가짐을 의미.
• B : sB — B가 소트 sB를 가지는 (아마 A와 다른) 타입임을 의미.

이 조건들 아래에서 의존 함수 타입 (x : A) → B : piSort sA (λ x → sB)를 만들 수 있어요. 이 타입 시그니처는 의존 함수 타입 (x : A) → B가 (아마 알려지지 않은) 그러나 잘 정의된 소트 piSort sA (λ x → sB)를 가지며, 정의역과 공역의 소트 측면에서 명시됨을 의미해요.

piSort가 어떻게 계산하는지에 대한 몇 가지 예제:

piSort s1       (λ x → s2)    = funSort s1 s2          (x가 s2에서 자유로이 발생하지 않으면)
piSort (Set ℓ)  (λ x → Set ℓ') = Setω                  (x가 ℓ'에서 엄격하게 발생하면)
piSort (Prop ℓ) (λ x → Set ℓ') = Setω                  (x가 ℓ'에서 엄격하게 발생하면)
piSort Setωᵢ    (λ x → Set ℓ') = Setωᵢ                 (x가 ℓ'에서 엄격하게 발생하면)

이 규칙들로 함수 타입 ∀ {A} → ∀ {B} → B → A → B(또는 더 명시적으로 {A : _9} {B : _7} → B → A → B)의 소트를 piSort (univSort _9) (λ A → funSort (univSort _7) (funSort _7 (funSort _9 _7)))로 계산할 수 있어요.

더 많은 예제:

piSort LevelUniv (λ l → Set l) 은 Setω로 평가됨 (level universe 참고)
piSort (Set l) (λ _ → Set l') 은 Set (l ⊔ l')로 평가됨
piSort s (λ _ → Setωi) 은 funSort s Setωi로 평가됨

더 알아보기 (Learn more)

• Agda 문서: 소트 시스템 원문