7.2. The Universe Design Pattern🔗

Lean에서 다른 타입을 분류하는 Type, Type 3, Prop 같은 타입을 유니버스라고 한다. 그러나 유니버스라는 말은 데이터 타입으로 Lean 타입의 부분집합을 나타내고 함수로 데이터 타입의 생성자를 실제 타입으로 바꾸는 설계 패턴을 뜻하기도 한다. 이 데이터 타입의 값을 해당 타입의 코드라고 한다.

Lean의 내장 유니버스와 마찬가지로 이 패턴으로 구현한 유니버스는 사용 가능한 타입의 모음을 기술하는 타입이지만 그 방식은 다르다. Lean에는 다른 타입을 직접 기술하는 Type, Type 3, Prop 같은 타입이 있다. 이 구성을 러셀식 유니버스라고 한다. 이 절의 사용자 정의 유니버스는 모든 타입을 데이터로 나타내고, 코드를 실제 타입으로 해석하는 명시적 함수를 포함한다. 이 구성을 타르스키식 유니버스라고 한다. 종속 타입 이론에 기반한 Lean 같은 언어는 거의 항상 러셀식 유니버스를 사용하지만, 타르스키식 유니버스는 이런 언어에서 API를 정의하는 유용한 패턴이다.

사용자 정의 유니버스를 정의하면 API에 사용할 닫힌 타입 모음을 만들 수 있다. 타입 모음이 닫혀 있으므로 코드에 대한 재귀로 유니버스의 모든 타입에서 작동하는 프로그램을 만들 수 있다. 사용자 정의 유니버스의 한 예에는 Nat을 나타내는 nat 코드와 Bool을 나타내는 bool 코드가 있다:

inductive NatOrBool where
  | nat | bool

abbrev NatOrBool.asType (code : NatOrBool) : Type :=
  match code with
  | .nat => Nat
  | .bool => Bool

코드에 패턴 매칭을 적용하면 Vect의 생성자에 패턴 매칭을 적용해 예상 길이를 정제하는 것처럼 타입을 정제할 수 있다. 예를 들어 이 유니버스의 타입을 문자열에서 역직렬화하는 프로그램은 다음과 같이 작성할 수 있다:

def decode (t : NatOrBool) (input : String) : Option t.asType :=
  match t with
  | .nat => input.toNat?
  | .bool =>
    match input with
    | "true" => some true
    | "false" => some false
    | _ => none

t에 종속 패턴 매칭을 적용하면 예상 결과 타입 t.asType이 각각 NatOrBool.nat.asType과 NatOrBool.bool.asType로 정제되며, 이는 실제 타입 Nat과 Bool로 계산된다.

다른 데이터와 마찬가지로 코드도 재귀적일 수 있다. NestedPairs 타입은 쌍과 자연수 타입의 가능한 모든 중첩을 코드화한다:

inductive NestedPairs where
  | nat : NestedPairs
  | pair : NestedPairs → NestedPairs → NestedPairs

abbrev NestedPairs.asType : NestedPairs → Type
  | .nat => Nat
  | .pair t1 t2 => asType t1 × asType t2

이 경우 해석 함수 NestedPairs.asType은 재귀적이다. 따라서 이 유니버스에 BEq를 구현하려면 코드에 대한 재귀가 필요하다:

def NestedPairs.beq (t : NestedPairs) (x y : t.asType) : Bool :=
  match t with
  | .nat => x == y
  | .pair t1 t2 => beq t1 x.fst y.fst && beq t2 x.snd y.snd

instance {t : NestedPairs} : BEq t.asType where
  beq x y := t.beq x y

NestedPairs 유니버스의 모든 타입에 이미 BEq 인스턴스가 있어도 타입 클래스 탐색은 인스턴스 선언에서 데이터 타입의 가능한 모든 경우를 자동으로 검사하지 않는다. NestedPairs처럼 경우가 무한히 많을 수 있기 때문이다. Lean에 코드 재귀로 인스턴스를 찾는 방법을 설명하지 않고 BEq 인스턴스를 직접 사용하려 하면 오류가 발생한다:

instance {t : NestedPairs} : BEq t.asType where
  beq x y := failed to synthesize instance of type class
  BEq t.asType

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.x == y

failed to synthesize instance of type class
  BEq t.asType

Hint: Type class instance resolution failures can be inspected with the `set_option trace.Meta.synthInstance true` command.

오류 메시지의 t는 NestedPairs 타입의 알려지지 않은 값을 나타낸다.

7.2.1. Type Classes vs Universes🔗

타입 클래스는 필요한 인터페이스의 구현만 있으면 열린 타입 모음을 API에 사용할 수 있게 한다. 대부분의 경우 이것이 더 낫다. API의 모든 사용 사례를 미리 예측하기는 어렵고, 타입 클래스는 라이브러리 코드를 원래 작성자가 예상한 것보다 많은 타입에서 사용하게 하는 편리한 방법이다.

반면 타르스키식 유니버스는 미리 정한 타입 모음에서만 API를 사용할 수 있도록 제한한다. 이는 다음과 같은 상황에서 유용하다:

전달된 타입에 따라 함수가 매우 다르게 동작해야 할 때—타입 자체에는 패턴 매칭을 적용할 수 없지만 타입 코드를 매칭하는 것은 가능하다
외부 시스템이 제공할 수 있는 데이터 타입을 본질적으로 제한하고 추가 유연성이 필요하지 않을 때
일부 연산의 구현을 넘어 타입의 추가 속성이 필요할 때

타입 클래스는 Java나 C#의 인터페이스와 같은 상황에서 유용하고, 타르스키식 유니버스는 봉인 클래스가 쓰일 상황이지만 일반 귀납 데이터 타입을 사용할 수 없을 때 유용하다.

7.2.2. A Universe of Finite Types🔗

API에 사용할 수 있는 타입을 미리 정한 모음으로 제한하면 열린 API에서는 불가능한 연산을 수행할 수 있다. 예를 들어 보통 함수는 동등성을 비교할 수 없다. 같은 입력을 같은 출력에 대응시키는 함수는 같다고 보아야 한다. 이를 검사하는 데는 무한한 시간이 걸릴 수 있다. Nat → Bool 타입의 두 함수를 비교하려면 모든 Nat에 대해 함수가 같은 Bool을 반환하는지 검사해야 하기 때문이다.

즉 무한 타입에서 나오는 함수 자체가 무한하다. 함수를 표로 볼 수 있는데 인자 타입이 무한한 함수는 각 경우를 나타내기 위해 무한히 많은 행이 필요하다. 반면 유한 타입에서 나오는 함수는 표에 유한한 행만 필요하므로 유한하다. 인자 타입이 유한한 두 함수는 가능한 인자를 모두 열거하고 각각에 함수를 적용한 뒤 결과를 비교하여 동등성을 검사할 수 있다. 고차 함수의 동등성을 검사하려면 주어진 타입의 모든 함수를 생성해야 하며, 이를 위해 인자 타입의 각 원소를 결과 타입의 각 원소에 대응시킬 수 있도록 반환 타입도 유한해야 한다. 이는 빠른 방법은 아니지만 유한한 시간 안에 끝난다.

유한 타입을 나타내는 한 가지 방법은 유니버스를 사용하는 것이다:

inductive Finite where
  | unit : Finite
  | bool : Finite
  | pair : Finite → Finite → Finite
  | arr : Finite → Finite → Finite

abbrev Finite.asType : Finite → Type
  | .unit => Unit
  | .bool => Bool
  | .pair t1 t2 => asType t1 × asType t2
  | .arr dom cod => asType dom → asType cod

이 유니버스에서 arr 생성자는 함수 타입을 나타낸다. 함수 타입을 화살표(arrow)로 쓰므로 생성자 이름도 arr라고 한다.

이 유니버스의 두 값을 비교하는 방법은 NestedPairs 유니버스와 거의 같다. 중요한 차이는 arr 경우가 추가된 것이다. 이 경우 Finite.enumerate 도우미로 dom이 코드화한 타입의 모든 값을 생성하고 두 함수가 가능한 모든 입력에서 같은 결과를 반환하는지 검사한다:

def Finite.beq (t : Finite) (x y : t.asType) : Bool :=
  match t with
  | .unit => true
  | .bool => x == y
  | .pair t1 t2 => beq t1 x.fst y.fst && beq t2 x.snd y.snd
  | .arr dom cod =>
    dom.enumerate.all fun arg => beq cod (x arg) (y arg)

표준 라이브러리 함수 List.all은 리스트의 모든 원소에서 주어진 함수가 true를 반환하는지 검사한다. 이 함수로 불리언에 대한 함수의 동등성을 비교할 수 있다:

true#eval Finite.beq (.arr .bool .bool) (fun _ => true) (fun b => b == b)

true

표준 라이브러리 함수를 비교하는 데도 사용할 수 있다:

false#eval Finite.beq (.arr .bool .bool) (fun _ => true) not

false

함수 합성과 같은 도구로 만든 함수도 비교할 수 있다:

true#eval Finite.beq (.arr .bool .bool) id (not ∘ not)

true

이는 Finite 유니버스가 라이브러리가 만든 특수한 유사 타입이 아니라 Lean의 실제 함수 타입을 코드화하기 때문이다.

enumerate의 구현도 Finite 코드에 대한 재귀로 이루어진다.

def Finite.enumerate (t : Finite) : List t.asType :=
  match t with
  | .unit => [()]
  | .bool => [true, false]
  | .pair t1 t2 => t1.enumerate.product t2.enumerate
  | .arr dom cod => dom.functions cod.enumerate

Unit 경우에는 값이 하나뿐이다. Bool 경우에는 반환할 값이 true와 false 두 개다. 쌍의 경우 결과는 t1이 코드화한 타입의 값과 t2가 코드화한 타입의 값의 데카르트 곱이어야 한다. 즉 dom의 모든 값은 cod의 모든 값과 짝지어야 한다. 도우미 함수 List.product는 보통 재귀 함수로 작성할 수 있지만 여기서는 항등 모나드에서 for를 사용해 정의한다:

def List.product (xs : List α) (ys : List β) : List (α × β) := Id.run do
  let mut out : List (α × β) := []
  for x in xs do
    for y in ys do
      out := (x, y) :: out
  pure out.reverse

마지막으로 함수에 대한 Finite.enumerate 경우는 가능한 모든 반환값의 리스트를 인자로 받는 Finite.functions 도우미에 위임한다.

일반적으로 유한 타입에서 결과값 모음으로 가는 모든 함수를 생성하는 일은 함수의 표를 생성하는 것으로 생각할 수 있다. 각 함수는 각 입력에 출력을 할당하므로 가능한 인자가 k개이면 함수 표에는 k개의 행이 있다. 표의 각 행은 n개의 가능한 출력 중 하나를 고를 수 있으므로 생성할 수 있는 함수는 n ^ k개다.

다시 말해 유한 타입에서 어떤 값 리스트로 가는 함수를 생성하는 일은 유한 타입을 기술하는 코드에 대한 재귀다:

def Finite.functions
    (t : Finite)
    (results : List α) : List (t.asType → α) :=
  match t with

Unit에서 나가는 함수의 표에는 행이 하나만 있다. 가능한 입력이 하나뿐이므로 함수는 입력에 따라 서로 다른 결과를 고를 수 없다. 따라서 가능한 결과마다 함수 하나가 생성된다.

| .unit =>
  results.map fun r =>
    fun () => r

결과값이 n개이면 Bool에서 나오는 함수는 n^2개다. Bool → α 타입의 각 함수가 Bool을 사용해 두 α 중 하나를 고르기 때문이다:

| .bool =>
  (results.product results).map fun (r1, r2) =>
    fun
      | true => r1
      | false => r2

쌍에서 나오는 함수는 커링을 이용하여 생성할 수 있다. 쌍에서 나오는 함수를 쌍의 첫 원소를 받아 두 번째 원소를 기다리는 함수를 반환하는 함수로 바꿀 수 있다. 이렇게 하면 이 경우에 Finite.functions를 재귀적으로 사용할 수 있다:

| .pair t1 t2 =>
  let f1s := t1.functions <| t2.functions results
  f1s.map fun f =>
    fun (x, y) =>
      f x y

고차 함수를 생성하는 일은 조금 머리를 써야 한다. 각 고차 함수는 함수를 인자로 받는다. 이 인자 함수는 입력과 출력 동작을 기준으로 다른 함수와 구별할 수 있다. 일반적으로 고차 함수는 인자 함수를 가능한 모든 인자에 적용한 뒤 적용 결과에 따라 가능한 동작을 수행할 수 있다. 이는 고차 함수를 구성하는 방법을 제시한다:

인자 그 자체인 함수에 가능한 모든 인자의 리스트에서 시작하라.
가능한 각 인자에 대해 인자 함수를 적용한 관찰 결과로 나올 수 있는 모든 동작을 구성하라. 나머지 가능한 인자에 대한 재귀와 Finite.functions를 사용하면 된다. 재귀 결과가 나머지 인자를 관찰한 함수들을 나타내기 때문이다. Finite.functions는 현재 인자의 관찰 결과에 따라 이를 달성하는 모든 방법을 구성한다.
이 관찰에 대한 가능한 동작마다 현재 가능한 인자에 인자 함수를 적용하는 고차 함수를 구성하라. 그 결과를 관찰 동작에 전달한다.
재귀의 기저 사례는 각 결과값에 대해 아무것도 관찰하지 않는 고차 함수다. 인자 함수를 무시하고 결과값을 그대로 반환한다.

이 재귀 함수를 직접 정의하면 Lean이 함수 전체의 종료를 증명하지 못한다. 그러나 우측 폴드라는 더 간단한 재귀 형식을 사용하면 함수가 종료함을 종료 검사기에 명확히 알릴 수 있다. 우측 폴드는 세 인자를 받는다. 리스트의 머리와 꼬리에 대한 재귀 결과를 결합하는 단계 함수, 리스트가 비었을 때 반환할 기본값, 처리할 리스트다. 그런 다음 리스트를 분석하여 리스트의 각 ::을 단계 함수 호출로, []을 기본값으로 바꾼다:

def List.foldr (f : α → β → β) (default : β) : List α → β
  | []     => default
  | a :: l => f a (foldr f default l)

리스트의 Nat 합은 foldr로 구할 수 있다:

                [1, 2, 3, 4, 5].foldr (· + ·) 0(1 :: 2 :: 3 :: 4 :: 5 :: []).foldr (· + ·) 0(1 + 2 + 3 + 4 + 5 + 0)15

foldr를 사용하면 고차 함수를 다음과 같이 만들 수 있다:

| .arr t1 t2 =>
  let args := t1.enumerate
  let base :=
    results.map fun r =>
      fun _ => r
  args.foldr
    (fun arg rest =>
      (t2.functions rest).map fun more =>
        fun f => more (f arg) f)
    base

Finite.functions의 완전한 정의는 다음과 같다:

def Finite.functions
    (t : Finite)
    (results : List α) : List (t.asType → α) :=
  match t with
| .unit =>
  results.map fun r =>
    fun () => r
| .bool =>
  (results.product results).map fun (r1, r2) =>
    fun
      | true => r1
      | false => r2
| .pair t1 t2 =>
  let f1s := t1.functions <| t2.functions results
  f1s.map fun f =>
    fun (x, y) =>
      f x y
    | .arr t1 t2 =>
      let args := t1.enumerate
      let base :=
        results.map fun r =>
          fun _ => r
      args.foldr
        (fun arg rest =>
          (t2.functions rest).map fun more =>
            fun f => more (f arg) f)
        base

Finite.enumerate와 Finite.functions가 서로 호출하므로 mutual 블록에서 정의해야 한다. 즉 Finite.enumerate 정의 바로 앞에 mutual 키워드를 둔다:

mutual
  def Finite.enumerate (t : Finite) : List t.asType :=
    match t with

그리고 Finite.functions 정의 바로 뒤에 end 키워드를 둔다:

| .arr t1 t2 =>
      let args := t1.enumerate
      let base :=
        results.map fun r =>
          fun _ => r
      args.foldr
        (fun arg rest =>
          (t2.functions rest).map fun more =>
            fun f => more (f arg) f)
        base
end

이 함수 비교 알고리즘은 실용적이지 않다. 검사할 경우의 수가 지수적으로 증가한다. ((Bool × Bool) → Bool) → Bool처럼 단순한 타입도 65536개의 서로 다른 함수를 나타낸다. 왜 이렇게 많은가? 앞의 추론에 따라 타입 T가 나타내는 값의 수를 \left| T \right|로 쓰면 다음을 예상할 수 있다. \left| \left( \left( \mathtt{Bool} \times \mathtt{Bool} \right) \rightarrow \mathtt{Bool} \right) \rightarrow \mathtt{Bool} \right| 이다 \left|\mathrm{Bool}\right|^{\left| \left( \mathtt{Bool} \times \mathtt{Bool} \right) \rightarrow \mathtt{Bool} \right| }, 이는 2^{2^{\left| \mathtt{Bool} \times \mathtt{Bool} \right| }}, 이는 2^{2^4} 즉 65536이다. 중첩된 지수는 빠르게 커지므로 고차 함수가 많다.

7.2.3. Exercises🔗

Finite가 나타내는 타입의 임의의 값을 문자열로 바꾸는 함수를 작성하라. 함수는 그 표로 나타내라.
Empty 빈 타입을 Finite와 Finite.beq에 추가하라.
Option을 Finite와 Finite.beq에 추가하라.