5.5. Universes🔗

단순화를 위해 이 책은 지금까지 Lean의 중요한 기능인 유니버스를 드러내지 않고 넘어왔다. 유니버스는 다른 타입을 분류하는 타입이다. 그중 익숙한 두 가지가 Type과 Prop이다. Type은 Nat, String, Int → String × Char, IO Unit 같은 일반 타입을 분류한다. Prop은 참일 수도 거짓일 수도 있는 명제를 분류한다. 예를 들면 "nisse" = "elf"나 3 > 2가 있다. Prop의 타입은 Type이다:

Prop : Type#check Prop

Prop : Type

기술적인 이유로 이 두 가지보다 더 많은 유니버스가 필요하다. 특히 Type 자체는 Type일 수 없다. 그렇게 허용하면 논리적 역설을 구성할 수 있어 정리 증명기로서 Lean의 유용성이 훼손된다.

이에 대한 형식적 논증은 지라르의 역설(Girard's Paradox)로 알려져 있다. 이는 더 잘 알려진 러셀의 역설(Russell's Paradox)과 관련이 있으며, 러셀의 역설은 집합론 초기 버전이 무모순적이지 않음을 보이는 데 사용되었다. 이러한 집합론에서는 성질로 집합을 정의할 수 있다. 예를 들어 모든 빨간 것의 집합, 모든 과일의 집합, 모든 자연수의 집합, 심지어 모든 집합의 집합도 생각할 수 있다. 집합이 주어지면 어떤 원소가 그 안에 포함되는지 물을 수 있다. 예를 들어 파랑새는 모든 빨간 것의 집합에 포함되지 않지만, 모든 빨간 것의 집합은 모든 집합의 집합에 포함된다. 실제로 모든 집합의 집합은 자기 자신도 포함한다.

그렇다면 자기 자신을 포함하지 않는 모든 집합의 집합은 어떨까? 모든 빨간 것의 집합은 그 자체가 빨간 것이 아니므로, 이 집합은 모든 빨간 것의 집합을 포함한다. 모든 집합의 집합은 자기 자신을 포함하므로, 이 집합은 모든 집합의 집합을 포함하지 않는다. 그렇다면 이 집합은 자기 자신을 포함할까? 자기 자신을 포함한다면 자기 자신을 포함할 수 없다. 그러나 포함하지 않는다면 포함해야 한다.

이는 모순이며, 처음의 가정에 무언가 잘못이 있었음을 보여준다. 특히 임의의 성질을 제공해 집합을 구성하도록 허용하는 것은 지나치게 강력하다. 이후의 집합론에서는 역설을 제거하기 위해 집합의 형성을 제한한다.

이와 관련된 역설은 Type에 Type 타입을 부여하는 종속 타입 이론의 변형에서도 구성할 수 있다. Lean이 일관된 논리적 토대를 갖추고 수학 도구로 사용될 수 있으려면 Type에는 다른 타입이 있어야 한다. 이 타입을 Type 1이라고 한다:

Type : Type 1#check Type

Type : Type 1

마찬가지로 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이다. 특히 일반 타입을 가진 값에 대한 술어는 Prop에 있다는 뜻이다. 예를 들어 (n : Nat) → n = n + 0 타입은 Nat에서 자기 자신에 0을 더한 값과 같다는 증거로 가는 함수를 나타낸다. Nat이 Type에 있더라도 이 규칙 때문에 이 함수 타입은 Prop에 있다. 마찬가지로 Type이 Type 1에 있더라도 함수 타입 Type → 2 + 2 = 4는 여전히 Prop에 있다.

5.5.1. User Defined Types🔗

구조체와 귀납 데이터 타입은 특정 유니버스에 존재하도록 선언할 수 있다. 그러면 Lean은 각 데이터 타입이 자기 자신의 타입을 포함하지 못할 만큼 충분히 큰 유니버스에 있는지 확인하여 역설을 피한다. 예를 들어 다음 선언에서 MyList는 Type에 존재하도록 선언되며, 타입 인수 α도 마찬가지다:

inductive MyList (α : Type) : Type where
  | nil : MyList α
  | cons : α → MyList α → MyList α

MyList 자체는 Type → Type이다. 따라서 실제 타입을 담는 데 사용할 수 없다. 그렇게 하면 인수가 Type이 되는데, 이는 Type 1이기 때문이다:

def myListOfNat : MyList Application type mismatch: The argument
  Type
has type
  Type 1
of sort `Type 2` but is expected to have type
  Type
of sort `Type 1` in the application
  MyList TypeType :=
  .cons Nat .nil

Application type mismatch: The argument
  Type
has type
  Type 1
of sort `Type 2` but is expected to have type
  Type
of sort `Type 1` in the application
  MyList Type

인수가 Type 1이 되도록 MyList를 수정하면 Lean이 거부하는 정의가 된다:

inductive MyList (α : Type 1) : Type where
  | nil : MyList α
  Invalid universe level in constructor `MyList.cons`: Parameter has type
  α
at universe level
  2
which is not less than or equal to the inductive type's resulting universe level
  1| cons : α → MyList α → MyList α

Invalid universe level in constructor `MyList.cons`: Parameter has type
  α
at universe level
  2
which is not less than or equal to the inductive type's resulting universe level
  1

이 오류는 cons의 α 타입 인수가 MyList보다 더 큰 유니버스에서 오기 때문에 발생한다. MyList 자체를 Type 1에 두면 이 문제는 해결되지만, 이제 MyList를 Type을 기대하는 문맥에서 사용하기 불편해진다는 대가가 따른다.

데이터 타입을 허용할지 결정하는 구체적인 규칙은 다소 복잡하다. 일반적으로는 데이터 타입을 인수 중 가장 큰 것과 같은 유니버스에서 시작하는 것이 가장 쉽다. 그 뒤 Lean이 정의를 거부하면 유니버스 수준을 1만큼 높이면 대개 통과한다.

5.5.2. Universe Polymorphism🔗

특정 유니버스에서 데이터 타입을 정의하면 코드가 중복될 수 있다. Type → Type에 MyList를 두면 실제 타입의 리스트에 사용할 수 없다. Type 1 → Type 1에 두면 타입 리스트의 리스트에 사용할 수 없다. Type, Type 1, Type 2 등에 사용할 버전을 만들기 위해 데이터 타입을 복사해 붙이는 대신, 유니버스 다형성(universe polymorphism)이라는 기능으로 이 유니버스 어디에서나 인스턴스화할 수 있는 단일 정의를 작성할 수 있다.

일반적인 다형 타입은 정의에서 타입을 대신할 변수들을 사용한다. 이를 통해 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 Application type mismatch: The argument
  Type
has type
  Type 1
of sort `Type 2` but is expected to have type
  Type
of sort `Type 1` in the application
  Sum String TypeType := .inr Nat

Application type mismatch: The argument
  Type
has type
  Type 1
of sort `Type 2` but is expected to have type
  Type
of sort `Type 1` in the application
  Sum String Type

두 타입 인수의 유니버스 수준에 서로 다른 변수를 사용하고 결과 데이터 타입을 둘 중 더 큰 유니버스에 둔다고 선언하면 이 데이터 타입을 더 유연하게 만들 수 있다:

inductive Sum (α : Type u) (β : Type v) : Type (max u v) where
  | inl : α → Sum α β
  | inr : β → Sum α β

이를 통해 Sum을 서로 다른 유니버스의 인수와 함께 사용할 수 있다:

def stringOrType : Sum String Type := .inr Nat

Lean이 유니버스 수준을 기대하는 위치에서는 다음 중 무엇이든 허용된다:

0이나 1 같은 구체적인 수준
수준을 대신하는 변수, 예를 들어 u나 v
두 수준의 최댓값. 수준에 max를 적용해 쓴다.
수준 증가. + 1로 쓴다.

5.5.2.1. Writing Universe-Polymorphic Definitions🔗

지금까지 이 책에서 정의한 모든 데이터 타입은 데이터의 가장 작은 유니버스인 Type에 있었다. 이 책은 List와 Sum 같은 Lean 표준 라이브러리의 다형 데이터 타입을 소개할 때 유니버스 다형성이 아닌 버전을 만들었다. 실제 버전은 유니버스 다형성을 사용해 타입 수준 프로그램과 비타입 수준 프로그램 사이에서 코드를 재사용할 수 있게 한다.

유니버스 다형 타입을 작성할 때 따를 일반 지침이 몇 가지 있다. 먼저 서로 독립적인 타입 인수에는 서로 다른 유니버스 변수를 사용해야 한다. 그러면 다형 정의를 더 다양한 인수와 함께 사용할 수 있어 코드 재사용 가능성이 커진다. 둘째, 전체 타입 자체는 일반적으로 모든 유니버스 변수의 최댓값에 있거나 그 최댓값보다 1 큰 수준에 있다. 먼저 둘 중 더 작은 쪽을 시도하라. 마지막으로 새 타입을 가능한 한 작은 유니버스에 두는 것이 좋다. 그러면 다른 문맥에서 더 유연하게 사용할 수 있다. Nat과 String 같은 비다형 타입은 Type 0에 직접 둘 수 있다.

5.5.2.2. `Prop` and Polymorphism🔗

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. Polymorphism in Practice🔗

이 책의 나머지 부분에서는 Lean 표준 라이브러리와 일관되도록 다형 데이터 타입, 구조체, 클래스의 정의에 유니버스 다형성을 사용한다. 이를 통해 Functor, Applicative, Monad 클래스의 전체 설명을 실제 정의와 완전히 일치시킬 수 있다.