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가 그러한 것과 동일한 이유로, Prop이 List에 제공하기에 적합한 인자임을 의미합니다. 명제의 목록은 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 사이에서 최대한 이식 가능하게 작성해야 하는 코드를 작성할 때 Prop을 반환하는 함수에 대한 특수 규칙을 Type 유니버스와 함께 사용할 수 있게 해줍니다.
5.5.3. 실전에서의 다형성
이 책의 나머지 부분에서는 다형적 데이터 타입, 구조체, 클래스의 정의가 Lean 표준 라이브러리와의 일관성을 위해 유니버스 다형성을 사용합니다. 이는 Functor, Applicative, Monad 클래스의 전체 설명이 실제 정의와 완전히 일치하도록 해 줍니다.