7.2. 유니버스 설계 패턴
Lean에서 Type, Type 3, Prop처럼 다른 타입을 분류하는 타입을 유니버스라고 합니다. 하지만 universe라는 용어는 자료형(datatype)을 사용하여 Lean 타입의 부분집합을 나타내고, 함수가 그 자료형의 생성자를 실제 타입으로 변환하는 디자인 패턴을 가리키는 데에도 사용됩니다. 이 데이터 타입의 값은 해당 타입에 대한 코드라고 불립니다.
Lean의 내장 유니버스와 마찬가지로, 이 패턴으로 구현된 유니버스는 사용 가능한 타입들의 어떤 모음을 기술하는 타입이지만, 그것이 이루어지는 메커니즘은 다릅니다. Lean에는 Type, Type 3, Prop처럼 다른 타입을 직접 기술하는 타입들이 있습니다. 이러한 배치는 Russell식 유니버스라고 불립니다. 이 절에서 설명하는 사용자 정의 유니버스는 자신의 모든 타입을 데이터로 표현하며, 이러한 코드를 실제 진짜 타입으로 해석하는 명시적 함수를 포함합니다. 이러한 구성은 타르스키식 유니버스라고 부릅니다. 의존 타입 이론에 기반한 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 := x == y
오류 메시지의 t는 NestedPairs 타입의 알 수 없는 값을 나타냅니다.
7.2.1. 타입 클래스와 유니버스
타입 클래스는 필요한 인터페이스의 구현이 있기만 하면 개방된 타입 집합을 API와 함께 사용할 수 있게 해줍니다. 대부분의 경우 이 방식이 더 바람직합니다. API의 모든 사용 사례를 미리 예측하는 것은 어려운 일이며, 타입 클래스는 라이브러리 코드가 원래 작성자가 예상했던 것보다 더 많은 타입에 사용될 수 있도록 해주는 편리한 방법입니다.
반면 타르스키식 유니버스는 API를 미리 정해진 타입들의 모음에서만 사용할 수 있도록 제한합니다. 이는 몇 가지 상황에서 유용합니다:
-
함수가 전달받은 타입에 따라 매우 다르게 동작해야 하는 경우—타입 자체에 대해서는 패턴 매칭을 할 수 없지만, 타입에 대한 코드에 대해서는 패턴 매칭이 허용됩니다
-
외부 시스템이 제공될 수 있는 데이터의 타입을 본질적으로 제한하며, 추가적인 유연성이 필요하지 않은 경우
-
어떤 연산의 구현뿐만 아니라 타입에 대한 추가적인 속성이 요구되는 경우
타입 클래스는 Java나 C#의 인터페이스와 많은 경우 유사하게 유용하지만, 타르스키식 유니버스는 sealed 클래스가 쓰일 법한 경우, 즉 일반적인 귀납적 타입은 사용할 수 없는 경우에 유용할 수 있습니다.
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은 함수 타입을 나타내며, 이는 화살표(arrarrow)로 표기됩니다.
이 유니버스에서 두 값이 같은지 비교하는 것은 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) 있습니다. 쌍(pair)에 대한 경우, 결과는 t1이 코딩하는 타입의 값들과 t2가 코딩하는 타입의 값들의 데카르트 곱(Cartesian product)이어야 합니다. 다시 말해, dom의 모든 값은 cod의 모든 값과 짝지어져야 합니다. 헬퍼 함수 List.product는 물론 일반적인 재귀 함수로도 작성할 수 있지만, 여기서는 항등 모나드(identity monad)에서 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
커링(currying)을 활용하면 쌍으로부터 함수를 생성할 수 있습니다. 쌍(pair)을 인자로 받는 함수는 쌍의 첫 번째 원소를 받아 두 번째 원소를 기다리는 함수를 반환하는 함수로 변환될 수 있습니다. 이렇게 하면 이 경우 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이 되리라 예상할 수 있습니다. 중첩된 지수는 빠르게 증가하며, 고차 함수도 많이 존재합니다.