5.5. 유니버스
이 책에서는 단순함을 위해 지금까지 Lean의 중요한 기능 하나를 짚지 않고 넘어갔습니다. 바로 유니버스입니다. 유니버스는 다른 타입을 분류하는 타입입니다. 그중 두 가지는 이미 익숙합니다. 바로 Type과 Prop입니다. Type은 Nat, String, Int → String × Char, IO Unit과 같은 일반적인 타입을 분류합니다. Prop은 "nisse" = "elf"나 3 > 2처럼 참일 수도 있고 거짓일 수도 있는 명제를 분류합니다. Prop의 타입은 Type입니다:
#check Prop
기술적인 이유로 이 두 유니버스보다 더 많은 유니버스가 필요합니다. 특히 Type 자체는 Type일 수 없습니다. 만약 그럴 수 있다면 논리적 역설을 만들어 낼 수 있게 되어 정리 증명기로서 Lean의 유용성이 훼손될 것입니다.
이에 대한 형식적 인자, 즉 논증은 지라르의 역설(Girard's Paradox)로 알려져 있습니다. 이는 더 잘 알려진 역설인 러셀의 역설(Russell's Paradox)과 관련이 있으며, 러셀의 역설은 초기 형태의 집합론이 모순적임을 보이는 데 사용되었습니다. 이러한 집합론에서는 성질을 통해 집합을 정의할 수 있습니다. 예를 들어, 모든 빨간 것의 집합, 모든 과일의 집합, 모든 자연수의 집합, 심지어 모든 집합의 집합도 있을 수 있습니다. 어떤 집합이 주어지면, 특정 원소가 그 집합에 포함되는지 물을 수 있습니다. 예를 들어, 파랑새는 모든 빨간 것의 집합에 포함되지 않지만, 모든 빨간 것의 집합은 모든 집합의 집합에 포함됩니다. 실제로 모든 집합의 집합은 자기 자신까지도 포함합니다.
그렇다면 자기 자신을 포함하지 않는 모든 집합의 집합은 어떻습니까? 이 집합은 모든 빨간 것의 집합을 포함합니다. 모든 빨간 것의 집합 자체는 빨갛지 않기 때문입니다. 이 집합은 모든 집합의 집합을 포함하지 않습니다. 모든 집합의 집합은 자기 자신을 포함하기 때문입니다. 그렇다면 이 집합은 자기 자신을 포함합니까? 자기 자신을 포함한다면, 이 집합은 자기 자신을 포함할 수 없습니다. 하지만 포함하지 않는다면, 반드시 포함해야 합니다.
이는 모순이며, 처음의 가정에 무언가 잘못이 있었음을 보여 줍니다. 특히, 임의의 속성을 제시하는 것만으로 집합을 구성할 수 있도록 허용하는 것은 지나치게 강력합니다. 이후의 집합론에서는 이 역설을 없애기 위해 집합의 형성을 제한합니다.
관련된 역설은 Type에 Type이라는 타입을 부여하는 의존 타입 이론 버전에서도 만들 수 있습니다. Lean이 일관된 논리적 기반을 갖추고 수학 도구로 쓰일 수 있으려면 Type은 다른 어떤 타입을 가져야 합니다. 이 타입을 Type 1이라고 부릅니다:
#check Type
마찬가지로 Type 1은 Type 2이고, Type 2는 Type 3이며, Type 3은 Type 4이고, 이런 식으로 계속됩니다.
함수 타입은 인자 타입과 반환 타입을 모두 담을 수 있는 가장 작은 유니버스에 속합니다. 즉, Nat → Nat은 Type이고, Type → Type은 Type 1이며, Type 1 → Type 2는 Type 3입니다.
이 규칙에는 한 가지 예외가 있습니다. 함수의 반환 타입이 Prop이면, 인자가 Type이나 심지어 Type 1처럼 더 큰 유니버스에 속하더라도 함수 타입 전체는 Prop에 속합니다. 특히 이는 일반적인 타입을 가진 값에 대한 술어(predicate)가 Prop에 속한다는 뜻입니다. 예를 들어, (n : Nat) → n = n + 0 타입은 Nat에서 그 값이 자기 자신에 0을 더한 값과 같다는 증거로 가는 함수를 나타냅니다. Nat은 Type에 속하지만, 이 규칙 때문에 이 함수 타입은 Prop에 속합니다. 마찬가지로 Type은 Type 1에 속하지만, 함수 타입 Type → 2 + 2 = 4는 여전히 Prop에 속합니다.
5.5.1. 사용자 정의 타입
구조체와 귀납적 데이터 타입은 특정 유니버스에 속하도록 선언할 수 있습니다. 그러면 Lean은 각 데이터 타입이 자기 자신의 타입을 포함할 수 없을 만큼 충분히 큰 유니버스에 속해 있어 역설을 피하는지 검사합니다. 예를 들어, 다음 선언에서 MyList는 Type에 속하도록 선언되며, 그 타입 인자 α도 마찬가지입니다:
inductive MyList (α : Type) : Type where
| nil : MyList α
| cons : α → MyList α → MyList α
MyList 자체는 Type → Type입니다. 즉, 실제 타입을 담는 데는 사용할 수 없습니다. 그렇게 하면 인자가 Type이 되는데, 이것은 Type 1이기 때문입니다:
def myListOfNat : MyList Type :=
.cons Nat .nil
MyList의 인자가 Type 1이 되도록 수정하면, Lean이 그 정의를 거부합니다:
inductive MyList (α : Type 1) : Type where
| nil : MyList α
| cons : α → MyList α → MyList α
이 오류는 cons에 전달되는 α 타입의 인자가 MyList보다 더 큰 유니버스에 속하기 때문에 발생합니다. MyList 자체를 Type 1에 두면 이 문제가 해결되지만, 그 대가로 이제 MyList 자체를 Type을 기대하는 문맥에서 사용하기가 불편해집니다.
데이터 타입이 허용되는지를 결정하는 구체적인 규칙은 다소 복잡합니다. 일반적으로는 데이터 타입을 인자 중 가장 큰 것과 같은 유니버스에 두고 시작하는 것이 가장 쉽습니다. 그런 다음 Lean이 정의를 거부하면 레벨을 하나 올리십시오. 대개는 그렇게 하면 통과합니다.
5.5.2. 유니버스 다형성
특정 유니버스에 데이터 타입을 정의하면 코드 중복이 생길 수 있습니다. MyList를 Type → Type에 두면 실제 타입들의 리스트에는 사용할 수 없습니다. Type 1 → Type 1에 두면 타입들의 리스트로 이루어진 리스트에는 사용할 수 없습니다. 데이터 타입을 복사해 붙여 넣어 Type, Type 1, Type 2 등에 해당하는 버전을 각각 만드는 대신, 유니버스 다형성이라는 기능을 사용하면 이 유니버스들 중 어디에서든 인스턴스화할 수 있는 단일 정의를 작성할 수 있습니다.
일반적인 다형 타입은 정의에서 타입을 나타내기 위해 변수를 사용합니다. 이를 통해 Lean은 변수를 상황에 따라 다르게 채울 수 있으며, 덕분에 이러한 정의를 다양한 타입과 함께 사용할 수 있습니다. 마찬가지로, 유니버스 다형성은 정의에서 변수가 유니버스를 나타낼 수 있게 해 줍니다. 이를 통해 Lean은 이 변수들을 상황에 따라 다르게 채울 수 있으므로, 정의를 다양한 유니버스와 함께 사용할 수 있습니다. 타입 인자에 관례적으로 그리스 문자로 이름을 붙이는 것처럼, 유니버스 인자에는 관례적으로 u, v, w라는 이름을 붙입니다.
이 MyList 정의는 특정 유니버스 레벨을 명시하지 않고, 대신 어떤 레벨이든 나타낼 수 있는 변수 u를 사용합니다. 이렇게 만든 데이터 타입을 Type과 함께 사용하면 u는 0이 되고, Type 3과 함께 사용하면 u는 3이 됩니다:
inductive MyList (α : Type u) : Type u where
| nil : MyList α
| cons : α → MyList α → MyList α
이 정의를 사용하면 MyList라는 하나의 정의로 실제 자연수와 자연수 타입 자체를 모두 담을 수 있습니다:
def myListOfNumbers : MyList Nat :=
.cons 0 (.cons 1 .nil)
def myListOfNat : MyList Type :=
.cons Nat .nil심지어 자기 자신을 포함할 수도 있습니다:
def myListOfList : MyList (Type → Type) :=
.cons MyList .nil
이렇게 하면 논리적 역설을 작성할 수 있을 것처럼 보입니다. 결국 유니버스 체계의 핵심 목적은 자기 참조적인 타입을 배제하는 것이기 때문입니다. 그러나 내부적으로는 MyList가 나타날 때마다 유니버스 레벨 인자가 주어집니다. 본질적으로 MyList의 유니버스 다형적 정의는 각 레벨마다 해당 데이터 타입의 사본을 만들어 낸 것이며, 레벨 인자는 그중 어떤 사본을 사용할지 선택합니다. 이러한 레벨 인자는 점과 중괄호로 표기하므로 MyList.{0} : Type → Type, MyList.{1} : Type 1 → Type 1, MyList.{2} : Type 2 → Type 2와 같이 됩니다.
레벨을 명시적으로 작성하면 앞의 예시는 다음과 같이 됩니다:
def myListOfNumbers : MyList.{0} Nat :=
.cons 0 (.cons 1 .nil)
def myListOfNat : MyList.{1} Type :=
.cons Nat .nil
def myListOfList : MyList.{1} (Type → Type) :=
.cons MyList.{0} .nil
유니버스 다형적 정의가 여러 타입을 인자로 받을 때는 유연성을 최대한 확보하기 위해 각 인자에 고유한 레벨 변수를 부여하는 것이 좋습니다. 예를 들어, 레벨 인자를 하나만 갖는 버전의 Sum은 다음과 같이 작성할 수 있습니다:
inductive Sum (α : Type u) (β : Type u) : Type u where
| inl : α → Sum α β
| inr : β → Sum α β이 정의는 여러 수준에서 사용할 수 있습니다:
def stringOrNat : Sum String Nat := .inl "hello"
def typeOrType : Sum Type Type := .inr Nat하지만 이를 사용하려면 두 인자가 같은 유니버스에 있어야 합니다:
def stringOrType : Sum String Type := .inr Nat두 타입 인자의 유니버스 레벨에 서로 다른 변수를 사용하고, 그 결과로 만들어지는 데이터 타입이 둘 중 더 큰 레벨에 속한다고 선언하면 이 데이터 타입을 더 유연하게 만들 수 있습니다:
inductive Sum (α : Type u) (β : Type v) : Type (max u v) where
| inl : α → Sum α β
| inr : β → Sum α β
이를 통해 Sum을 서로 다른 유니버스의 인자와 함께 사용할 수 있습니다:
def stringOrType : Sum String Type := .inr NatLean에서 유니버스 레벨이 필요한 위치에는 다음 중 어느 것이든 사용할 수 있습니다.
-
0이나1과 같은 구체적인 레벨 -
u나v처럼 레벨을 나타내는 변수 -
레벨에
max를 적용하여 표기하는 두 레벨의 최댓값 -
+ 1로 표기하는 레벨 증가
5.5.2.1. 유니버스 다형적 정의 작성하기
지금까지 이 책에서 정의한 모든 데이터 타입은 가장 작은 데이터 유니버스인 Type에 속했습니다. 이 책에서는 List나 Sum처럼 Lean 표준 라이브러리에 있는 다형적 데이터 타입을 소개할 때 유니버스 다형적이지 않은 버전을 따로 만들었습니다. 실제 버전은 유니버스 다형성을 사용하므로 타입 수준 프로그램과 타입 수준이 아닌 프로그램이 같은 코드를 재사용할 수 있습니다.
유니버스 다형 타입을 작성할 때 따라야 할 몇 가지 일반적인 지침이 있습니다. 첫째, 서로 독립적인 타입 인자에는 서로 다른 유니버스 변수를 사용해야 합니다. 그러면 다형적 정의를 더 다양한 인자와 함께 사용할 수 있으므로 코드를 재사용할 여지가 커집니다. 둘째, 타입 전체는 보통 모든 유니버스 변수의 최댓값에 해당하는 유니버스에 속하거나, 그 최댓값보다 하나 큰 유니버스에 속합니다. 둘 중 더 작은 쪽을 먼저 시도해 보십시오. 마지막으로, 새 타입은 가능한 한 작은 유니버스에 두는 것이 좋습니다. 그래야 다른 맥락에서 더 유연하게 사용할 수 있습니다. Nat나 String처럼 다형 타입이 아닌 타입은 Type 0에 바로 둘 수 있습니다.
5.5.2.2. Prop과 다형성
Type, Type 1 등이 프로그램과 데이터를 분류하는 타입을 기술하듯이, Prop은 논리적 명제를 분류합니다. Prop에 속하는 타입은 어떤 진술이 참이라는 것을 뒷받침하는 설득력 있는 증거로 무엇이 인정되는지를 기술합니다. 명제는 여러 면에서 일반적인 타입과 비슷합니다. 귀납적으로 선언할 수 있고, 생성자를 가질 수 있으며, 함수가 명제를 인자로 받을 수도 있습니다. 그러나 데이터 타입과 달리, 일반적으로 진술이 참이라는 증거로 어떤 증거가 제시되는지는 중요하지 않으며, 증거가 제시된다는 사실만이 중요합니다. 반면에 프로그램은 Nat을 반환하는 것만으로는 부족하며, 그것이 올바른 Nat이어야 한다는 점이 매우 중요합니다.
Prop은 유니버스 계층의 가장 아래에 있으며, Prop의 타입은 Type입니다. 즉, Nat이 List에 넘기기에 적합한 인자인 것과 같은 이유로 Prop도 적합한 인자입니다. 명제의 리스트는 List Prop 타입을 가집니다:
def someTruePropositions : List Prop := [
1 + 1 = 2,
"Hello, " ++ "world!" = "Hello, world!"
]
유니버스 인자를 명시적으로 채워 넣으면 Prop이 Type임을 확인할 수 있습니다:
def someTruePropositions : List.{0} Prop := [
1 + 1 = 2,
"Hello, " ++ "world!" = "Hello, world!"
]
내부적으로 Prop과 Type은 Sort라는 하나의 계층으로 통합되어 있습니다. Prop은 Sort 0과 같고, Type 0은 Sort 1, Type 1은 Sort 2이며, 그 이후도 마찬가지입니다. 실제로 Type u는 Sort (u+1)과 같습니다. Lean으로 프로그램을 작성할 때 이 사실은 대개 중요하지 않습니다. 하지만 오류 메시지에 가끔 나타날 수 있으며, CoeSort 클래스의 이름도 여기에서 비롯되었습니다. 또한 Prop이 Sort 0이기 때문에 유니버스 연산자 하나를 더 유용하게 쓸 수 있습니다. 유니버스 레벨 imax u v는 v가 0이면 0이고, 그렇지 않으면 u와 v 중 더 큰 값입니다. 이 연산자를 Sort와 함께 사용하면, Prop 유니버스와 Type 유니버스 사이에서 최대한 이식성이 높아야 하는 코드를 작성할 때 Prop을 반환하는 함수에 대한 특별 규칙을 적용할 수 있습니다.
5.5.3. 실전에서의 다형성
이 책의 나머지 부분에서는 Lean 표준 라이브러리와 일관성을 유지하기 위해 다형적 데이터 타입, 구조체, 클래스를 정의할 때 유니버스 다형성을 사용합니다. 이렇게 하면 Functor, Applicative, Monad 클래스 전체를 실제 정의와 완전히 일치하는 형태로 제시할 수 있습니다.