7.2. 유니버스 디자인 패턴
Lean에서 Type, Type 3, Prop처럼 다른 타입을 분류하는 타입을 유니버스라고 합니다. 그러나 유니버스라는 용어는 데이터 타입으로 Lean 타입의 부분집합을 표현하고 함수가 그 데이터 타입의 생성자를 실제 타입으로 변환하는 디자인 패턴을 가리킬 때에도 쓰입니다. 이 데이터 타입의 값을 해당 타입의 코드라고 합니다.
Lean의 내장 유니버스와 마찬가지로, 이 패턴으로 구현한 유니버스도 사용할 수 있는 타입들의 어떤 모음을 기술하는 타입입니다. 다만 그렇게 하는 방식은 서로 다릅니다. Lean에는 Type, Type 3, Prop처럼 다른 타입을 직접 기술하는 타입들이 있습니다. 이러한 방식을 러셀식 유니버스(universes à la Russell)라고 부릅니다. 이 절에서 설명하는 사용자 정의 유니버스는 자신의 모든 타입을 데이터로 표현하며, 이러한 코드를 진짜 실제 타입으로 해석하는 명시적인 함수를 포함합니다. 이러한 방식을 타르스키식 유니버스(universes à la Tarski)라고 부릅니다. 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처럼 그러한 경우가 무한히 많을 수 있기 때문입니다. 코드에 대한 재귀로 BEq 인스턴스를 찾는 방법을 Lean에 설명하는 대신 해당 인스턴스를 직접 사용하려고 하면 오류가 발생합니다:
instance {t : NestedPairs} : BEq t.asType where
beq x y := x == y
오류 메시지의 t는 NestedPairs 타입의 알 수 없는 값을 나타냅니다.
7.2.1. 타입 클래스와 유니버스
타입 클래스를 사용하면 필요한 인터페이스의 구현을 갖추기만 한 타입이라면 어떤 타입이든 API와 함께 사용할 수 있으며, 이러한 타입의 집합은 열려 있습니다. 대부분의 경우에는 이 방식이 더 바람직합니다. API의 모든 사용 사례를 미리 예측하기는 어려우며, 타입 클래스는 라이브러리 코드를 원래 작성자가 예상한 것보다 더 많은 타입과 함께 사용할 수 있게 해 주는 편리한 방법입니다.
반면 타르스키식 유니버스(universe à la Tarski)는 미리 정해진 타입 모음에서만 API를 사용할 수 있도록 제한합니다. 이는 몇 가지 상황에서 유용합니다.
-
함수가 전달받는 타입에 따라 매우 다르게 동작해야 할 때—타입 자체에 대해서는 패턴 매칭을 할 수 없지만, 타입을 나타내는 코드에 대해서는 패턴 매칭을 할 수 있습니다
-
외부 시스템이 제공할 수 있는 데이터의 타입을 본질적으로 제한하며 추가적인 유연성이 필요하지 않은 경우
-
일부 연산의 구현 외에 타입에 추가적인 속성이 요구되는 경우
타입 클래스는 Java나 C#의 인터페이스가 쓰이는 여러 상황에서 마찬가지로 유용하며, 타르스키식 유니버스(universe à la Tarski)는 봉인 클래스(sealed class)를 사용할 법하지만 일반적인 귀납적 데이터 타입은 사용할 수 없는 경우에 유용할 수 있습니다.
7.2.2. 유한 타입의 유니버스
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)로 표기합니다.
이 유니버스의 두 값이 같은지 비교하는 방법은 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를 반환하는지 확인합니다. 이 함수를 사용하면 불리언 함수끼리 서로 같은지 비교할 수 있습니다:
#eval Finite.beq (.arr .bool .bool) (fun _ => true) (fun b => b == b)표준 라이브러리의 함수들을 비교하는 데에도 사용할 수 있습니다:
#eval Finite.beq (.arr .bool .bool) (fun _ => true) not함수 합성 같은 도구로 만든 함수까지도 비교할 수 있습니다:
#eval Finite.beq (.arr .bool .bool) id (not ∘ not)
이는 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이 될 것이라고 예상할 수 있습니다. 중첩된 지수는 빠르게 커지며, 고차 함수는 매우 많습니다.