3.5. 표준 클래스
이 절에서는 Lean에서 타입 클래스를 사용하여 오버로딩할 수 있는 다양한 연산자와 함수를 소개합니다. 각 연산자 또는 함수는 타입 클래스의 메서드에 대응합니다. C++와 달리, Lean의 중위 연산자는 이름 붙은 함수의 축약형으로 정의됩니다. 이는 새로운 타입에 대해 이를 오버로딩하는 것이 연산자 자체를 이용해서가 아니라, (HAdd.hAdd와 같이) 그 기저에 있는 이름을 이용해서 이루어짐을 의미합니다.
3.5.1. 산술 연산
대부분의 산술 연산자는 이형(heterogeneous) 형태로도 제공되는데, 이 경우 인자들이 서로 다른 타입을 가질 수 있으며 출력 매개변수가 결과 표현식의 타입을 결정합니다. 각 이형(異形) 연산자에는 h라는 글자를 제거하여 찾을 수 있는 동형(同形) 버전이 대응됩니다. 예를 들어 HAdd.hAdd는 Add.add가 됩니다. 다음 산술 연산자들은 오버로드되어 있습니다:
표현식 | 탈설탕화(Desugaring) | 클래스 이름 |
|---|---|---|
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
3.5.2. 비트 연산자
Lean은 타입 클래스를 사용하여 오버로딩된 여러 표준 비트 연산자를 포함하고 있습니다. UInt8, UInt16, UInt32, UInt64, USize와 같은 고정폭 타입에 대한 인스턴스가 있습니다. 후자는 현재 플랫폼에서 워드의 크기로, 일반적으로 32비트 또는 64비트입니다. 다음 비트 연산자들이 오버로드되어 있습니다:
표현식 | 탈설탕화 | 클래스 이름 |
|---|---|---|
|
| |
|
| |
|
| |
|
|
|
| ||
|
And와 Or라는 이름은 이미 논리 연결사의 이름으로 사용되고 있기 때문에, HAnd와 HOr의 동종(homogeneous) 버전은 And와 Or가 아니라 AndOp와 OrOp라고 불립니다.
3.5.3. 동등성과 순서
두 값의 동등성을 테스트할 때는 일반적으로 BEq 클래스를 사용하는데, 이는 “Boolean equality(불리언 동등성)”의 줄임말입니다. Lean이 정리 증명기로 사용된다는 특성으로 인해, Lean에는 실질적으로 두 가지 종류의 동등성 연산자가 존재합니다.
-
불리언 동등성은 다른 프로그래밍 언어에서도 찾아볼 수 있는 것과 같은 종류의 동등성입니다. 이는 두 값을 받아
Bool을 반환하는 함수입니다. 불리언 동등성은 Python과 C#에서와 마찬가지로 등호 두 개로 표기합니다. Lean은 순수 함수형 언어이므로, 참조 동등성과 값 동등성이라는 별개의 개념이 존재하지 않습니다—포인터는 직접 관찰할 수 없습니다. -
명제적 동등성은 두 대상이 같다는 수학적 명제입니다. 명제적 동등성은 함수가 아니라, 오히려 증명을 허용하는 수학적 명제입니다. 이는 등호 하나로 표기됩니다. 명제적 동등성을 나타내는 명제는 이 동등성에 대한 증거를 분류하는 타입과 같습니다.
두 가지 동등성 개념 모두 중요하며, 서로 다른 목적으로 사용됩니다. 불리언 동등성은 두 값이 같은지 여부에 대한 판단이 필요할 때 프로그램에서 유용합니다. 예를 들어, "Octopus" == "Cuttlefish"는 false로 평가되고, "Octopodes" == "Octo".append "podes"는 true로 평가됩니다. 함수와 같은 일부 값은 동등성을 검사할 수 없습니다. 예를 들어, (fun (x : Nat) => 1 + x) == (Nat.succ ·)는 다음 오류를 발생시킵니다:
이 메시지가 나타내듯이, ==는 타입 클래스를 사용하여 오버로드됩니다. x == y 표현식은 사실 BEq.beq x y의 축약형입니다.
명제적 동등성은 프로그램의 실행이라기보다는 수학적 진술입니다. 명제는 어떤 진술에 대한 증거를 기술하는 타입과 비슷하기 때문에, 명제적 동등성은 불리언 동등성보다는 String이나 Nat → List Int와 같은 타입과 더 공통점이 많습니다. 이는 자동으로 검사될 수 없다는 것을 의미합니다. 하지만 두 식이 같은 타입을 가지는 한, 이들의 동등성은 Lean에서 서술될 수 있습니다. (fun (x : Nat) => 1 + x) = (Nat.succ ·) 라는 명제문은 완벽하게 타당한 명제문입니다. 수학적 관점에서는 두 함수가 동일한 입력을 동일한 출력으로 대응시킨다면 서로 같다고 보므로, 이 문장은 참이기까지 합니다. 다만 Lean이 이 사실을 납득하게 하려면 한 줄짜리 증명이 필요합니다.
일반적으로, Lean을 프로그래밍 언어로 사용할 때는 명제보다 부울 함수를 고수하는 것이 가장 쉽습니다. 하지만 Bool의 생성자 이름이 true와 false인 것에서 알 수 있듯이, 이 차이는 때때로 모호해집니다. 일부 명제는 결정 가능한데, 이는 불리언 함수처럼 검사할 수 있음을 의미합니다. 명제가 참인지 거짓인지 확인하는 함수를 decision procedure라고 하며, 이 함수는 명제의 참 또는 거짓에 대한 evidence를 반환합니다. 결정 가능한 명제의 예로는 자연수의 동등성 및 부등성, 문자열의 동등성, 그리고 그 자체로 결정 가능한 명제들의 "그리고"와 "또는" 등이 있습니다.
Lean에서 if는 결정 가능한 명제와 함께 작동합니다. 예를 들어, 2 < 4는 명제입니다:
#check 2 < 4
그럼에도 불구하고, 이를 if의 조건으로 작성하는 것은 완전히 허용됩니다. 예를 들어, if 2 < 4 then 1 else 2는 Nat 타입을 가지며 1로 평가됩니다.
모든 명제가 결정 가능한 것은 아닙니다. 만약 그렇다면 컴퓨터는 결정 절차를 실행하는 것만으로 참인 명제를 모두 증명할 수 있을 것이고, 수학자들은 일자리를 잃게 될 것입니다. 더 구체적으로, 결정 가능한 명제는 결정 절차를 담고 있는 Decidable 타입 클래스의 인스턴스를 가집니다. 결정 가능하지 않은 명제를 Bool인 것처럼 사용하려 하면 Decidable 인스턴스를 찾지 못해 실패하게 됩니다. 예를 들어, if (fun (x : Nat) => 1 + x) = (Nat.succ ·) then "yes" else "no"의 결과는 다음과 같습니다:
일반적으로 결정 가능한 다음 명제들은 타입 클래스로 오버로드되어 있습니다:
표현식 | 탈설탕화 | 클래스 이름 |
|---|---|---|
|
| |
|
| |
|
| |
|
|
새로운 명제를 정의하는 방법이 아직 설명되지 않았으므로, LT와 LE의 완전히 새로운 인스턴스를 정의하는 것은 어려울 수 있습니다. 하지만 기존 인스턴스를 이용해 정의할 수 있습니다. Pos에 대한 LT와 LE 인스턴스는 Nat에 대한 기존 인스턴스를 사용할 수 있습니다:
instance : LT Pos where
lt x y := LT.lt x.toNat y.toNatinstance : LE Pos where
le x y := LE.le x.toNat y.toNat
Lean이 인스턴스를 합성하는 동안 명제의 정의를 펼치지 않기 때문에, 이 명제들은 기본적으로 결정 가능하지 않습니다. 이는 inferInstance 연산자를 사용하여 연결할 수 있는데, 이 연산자는 인스턴스가 존재하는 경우 이를 찾아냅니다. 타입 표기는 inferInstance가 Decidable (x.toNat < y.toNat)와 Decidable (x.toNat ≤ y.toNat)의 인스턴스를 추론하도록 지시하며, 이는 펼쳐진 버전입니다:
instance {x : Pos} {y : Pos} : Decidable (x < y) :=
(inferInstance : Decidable (x.toNat < y.toNat))
instance {x : Pos} {y : Pos} : Decidable (x ≤ y) :=
(inferInstance : Decidable (x.toNat ≤ y.toNat))타입 검사기는 명제들의 정의가 일치하는지 확인합니다. 이들을 혼동하면 오류가 발생합니다:
instance {x : Pos} {y : Pos} : Decidable (x ≤ y) :=
(inferInstance : Decidable (x.toNat < y.toNat))
<, ==, >를 사용하여 값을 비교하는 것은 비효율적일 수 있습니다. 한 값이 다른 값보다 작은지 먼저 확인한 다음 두 값이 같은지 확인하는 것은 큰 데이터 구조에 대해 두 번의 순회를 필요로 할 수 있습니다. 이 문제를 해결하기 위해, Java와 C#은 각각 표준 compareTo와 CompareTo 메서드를 제공하며, 클래스가 이를 오버라이드하여 세 가지 연산을 동시에 구현할 수 있도록 합니다. 이 메서드들은 수신자가 인자보다 작으면 음의 정수를, 같으면 0을, 수신자가 인자보다 크면 양의 정수를 반환합니다. 정수의 의미를 오버로딩하는 대신, Lean은 이 세 가지 가능성을 기술하는 내장 귀납적 타입을 제공합니다:
inductive Ordering where
| lt
| eq
| gt
Ord 타입 클래스를 오버로딩하여 이러한 비교를 만들어 낼 수 있습니다. Pos의 경우, 구현은 다음과 같을 수 있습니다:
def Pos.comp : Pos → Pos → Ordering
| Pos.one, Pos.one => Ordering.eq
| Pos.one, Pos.succ _ => Ordering.lt
| Pos.succ _, Pos.one => Ordering.gt
| Pos.succ n, Pos.succ k => comp n k
instance : Ord Pos where
compare := Pos.comp
Java에서 compareTo가 올바른 접근 방식이 될 상황에서는, Lean에서 Ord.compare를 사용하십시오.
3.5.4. 해싱
Java와 C#에는 각각 해시 테이블과 같은 자료구조에 사용할 값의 해시를 계산하는 hashCode와 GetHashCode 메서드가 있습니다. Lean에서 이에 대응하는 것은 Hashable이라는 타입 클래스입니다:
class Hashable (α : Type) where
hash : α → UInt64
두 값이 해당 타입에 대한 BEq 인스턴스에 따라 동등하다고 간주된다면, 두 값은 동일한 해시를 가져야 합니다. 다시 말해, x == y이면 hash x == hash y입니다. x ≠ y인 경우, hash x가 hash y와 반드시 다르지는 않습니다(UInt64 값보다 Nat 값이 무한히 더 많으니 당연한 일입니다). 하지만 해시 기반 자료 구조는 서로 다른 값이 서로 다른 해시를 가질 가능성이 높을수록 더 나은 성능을 보입니다. 이는 Java 및 C#에서와 동일한 기대치입니다.
표준 라이브러리에는 생성자의 서로 다른 필드에 대한 해시를 결합하는 데 사용할 수 있는, 타입이 UInt64 → UInt64 → UInt64인 함수 mixHash가 있습니다. 귀납적 데이터 타입에 대한 합리적인 해시 함수는 각 생성자에 고유한 번호를 할당한 다음, 그 번호를 각 필드의 해시와 혼합함으로써 작성할 수 있습니다. 예를 들어, Pos에 대한 Hashable 인스턴스는 다음과 같이 작성할 수 있습니다:
def hashPos : Pos → UInt64
| Pos.one => 0
| Pos.succ n => mixHash 1 (hashPos n)
instance : Hashable Pos where
hash := hashPos
다형 타입에 대한 Hashable 인스턴스는 재귀적 인스턴스 검색을 사용할 수 있습니다. NonEmptyList α를 해싱하는 것은 α를 해싱할 수 있을 때만 가능합니다:
instance [Hashable α] : Hashable (NonEmptyList α) where
hash xs := mixHash (hash xs.head) (hash xs.tail)
이진 트리는 BEq와 Hashable의 구현에서 재귀와 재귀적 인스턴스 탐색을 모두 사용합니다:
inductive BinTree (α : Type) where
| leaf : BinTree α
| branch : BinTree α → α → BinTree α → BinTree α
def eqBinTree [BEq α] : BinTree α → BinTree α → Bool
| BinTree.leaf, BinTree.leaf =>
true
| BinTree.branch l x r, BinTree.branch l2 x2 r2 =>
x == x2 && eqBinTree l l2 && eqBinTree r r2
| _, _ =>
false
instance [BEq α] : BEq (BinTree α) where
beq := eqBinTree
def hashBinTree [Hashable α] : BinTree α → UInt64
| BinTree.leaf =>
0
| BinTree.branch left x right =>
mixHash 1
(mixHash (hashBinTree left)
(mixHash (hash x)
(hashBinTree right)))
instance [Hashable α] : Hashable (BinTree α) where
hash := hashBinTree3.5.5. 표준 클래스 유도하기
BEq, Hashable과 같은 클래스의 인스턴스는 직접 구현하기가 꽤 지루한 경우가 많습니다. Lean에는 컴파일러가 여러 타입 클래스에 대해 잘 동작하는 인스턴스를 자동으로 생성할 수 있게 해 주는 instance deriving이라는 기능이 포함되어 있습니다. 사실, 다형성에 대한 첫 번째 절에서 Firewood의 정의에 있는 deriving Repr 구절이 인스턴스 유도의 한 예입니다.
인스턴스는 두 가지 방식으로 유도할 수 있습니다. 첫 번째는 구조체나 귀납적 타입을 정의할 때 사용할 수 있습니다. 이 경우, 타입 선언의 끝에 deriving을 추가하고 그 뒤에 인스턴스가 파생되어야 할 클래스들의 이름을 붙이면 됩니다. 이미 정의된 타입에 대해서는 독립적인 deriving 명령을 사용할 수 있습니다. 나중에 타입 T에 대해 C1, C2, ...의 인스턴스를 유도하려면 deriving instance C1, C2, ... for T를 작성하십시오.
매우 적은 양의 코드를 사용하여 Pos와 NonEmptyList에 대해 BEq와 Hashable 인스턴스를 유도할 수 있습니다:
deriving instance BEq, Hashable for Pos
deriving instance BEq, Hashable for NonEmptyList최소한 다음 클래스들에 대해서는 인스턴스를 파생시킬 수 있습니다:
하지만 경우에 따라 파생된 Ord 인스턴스가 애플리케이션에서 원하는 순서를 정확히 만들어 내지 못할 수 있습니다. 이런 경우라면 Ord 인스턴스를 직접 작성해도 무방합니다. 인스턴스를 도출할 수 있는 클래스의 모음은 Lean의 고급 사용자가 확장할 수 있습니다.
프로그래머의 생산성과 코드 가독성 측면에서의 명확한 이점 외에도, 인스턴스를 파생시키는 것은 타입의 정의가 발전함에 따라 인스턴스도 함께 갱신되므로 코드를 유지 보수하기 더 쉽게 만들어줍니다. 코드 변경 사항을 검토할 때, 데이터타입 갱신과 관련된 수정은 동등성 검사와 해시 계산에 대한 정형화된 수정이 줄줄이 이어지지 않아야 훨씬 읽기 쉽습니다.
3.5.6. 이어붙이기
많은 데이터 타입은 일종의 추가(append) 연산자를 가지고 있습니다. Lean에서 두 값을 이어붙이는 연산은 타입 클래스 HAppend로 오버로드되어 있으며, 이는 산술 연산에 사용되는 것과 같은 이종(heterogeneous) 연산입니다:
class HAppend (α : Type) (β : Type) (γ : outParam Type) where
hAppend : α → β → γ
xs ++ ys 구문은 HAppend.hAppend xs ys로 탈설탕화됩니다. 동형(homogeneous) 경우에는 일반적인 패턴을 따르는 Append의 인스턴스를 구현하는 것으로 충분합니다:
instance : Append (NonEmptyList α) where
append xs ys :=
{ head := xs.head, tail := xs.tail ++ ys.head :: ys.tail }위 인스턴스를 정의한 후,
#eval idahoSpiders ++ idahoSpiders다음과 같은 출력을 갖습니다:
마찬가지로, HAppend의 정의는 비어 있지 않은 리스트를 일반 리스트에 이어붙일 수 있게 해줍니다:
instance : HAppend (NonEmptyList α) (List α) (NonEmptyList α) where
hAppend xs ys :=
{ head := xs.head, tail := xs.tail ++ ys }이 인스턴스가 사용 가능해지면,
#eval idahoSpiders ++ ["Trapdoor Spider"]결과는 다음과 같습니다
3.5.7. 펑터
다형 타입은 함수로 그 안에 포함된 모든 요소를 변환하는 map이라는 이름의 함수에 대한 오버로드를 가지고 있다면 펑터입니다. 대부분의 언어에서 이 용어를 사용하지만, C#에서 map에 해당하는 것은 System.Linq.Enumerable.Select라고 불립니다. 예를 들어, 리스트에 함수를 매핑하면 시작 리스트의 각 항목이 해당 항목에 함수를 적용한 결과로 대체된 새 리스트가 구성됩니다. Option에 함수 f를 매핑하면 none은 그대로 두고, some x를 some (f x)로 바꿉니다.
다음은 펑터의 몇 가지 예시와 이들의 Functor 인스턴스가 map을 오버로드하는 방식입니다:
-
Functor.map (· + 5) [1, 2, 3]는[6, 7, 8]로 평가됩니다 -
Functor.map toString (some (List.cons 5 List.nil))는some "[5]"로 평가됩니다. -
Functor.map List.reverse [[1, 2, 3], [4, 5, 6]]는[[3, 2, 1], [6, 5, 4]]로 평가됩니다
Functor.map는 이 흔한 연산을 나타내기에는 이름이 다소 길기 때문에, Lean은 함수를 매핑하기 위한 중위 연산자인 <$>도 제공합니다. 앞선 예제들은 다음과 같이 다시 작성할 수 있습니다:
-
(· + 5) <$> [1, 2, 3]은[6, 7, 8]로 평가됩니다 -
toString <$> (some (List.cons 5 List.nil))는some "[5]"로 평가됩니다 -
List.reverse <$> [[1, 2, 3], [4, 5, 6]]은[[3, 2, 1], [6, 5, 4]]로 평가됩니다
NonEmptyList에 대한 Functor 인스턴스는 map 함수를 지정해야 합니다.
instance : Functor NonEmptyList where
map f xs := { head := f xs.head, tail := f <$> xs.tail }
여기서 map은 List에 대한 Functor 인스턴스를 사용하여 함수를 꼬리 부분에 매핑합니다. 이 인스턴스는 NonEmptyList α가 아니라 NonEmptyList에 대해 정의되는데, 이는 인자 타입 α가 타입 클래스를 해소하는 데 아무런 역할을 하지 않기 때문입니다. NonEmptyList는 항목의 타입이 무엇이든 상관없이 함수를 매핑할 수 있습니다. 만약 α가 클래스의 매개변수였다면 NonEmptyList Nat에서만 작동하는 Functor의 버전을 만드는 것이 가능했겠지만, 펑터라는 것의 일부는 map이 어떤 항목 타입에 대해서도 작동한다는 것입니다.
다음은 PPoint에 대한 Functor의 인스턴스입니다:
instance : Functor PPoint where
map f p := { x := f p.x, y := f p.y }
이 경우, f는 x와 y 모두에 적용되었습니다.
펑터에 담긴 타입 자체가 펑터인 경우에도, 함수를 매핑하면 한 계층만 내려갑니다. 즉, NonEmptyList (PPoint Nat)에 map을 사용할 때, 매핑되는 함수는 Nat이 아니라 PPoint Nat을 인자로 받아야 합니다.
Functor 클래스의 정의는 아직 다루지 않은 언어 기능을 하나 더 사용합니다: 바로 기본 메서드 정의입니다. 일반적으로 클래스는 함께 사용했을 때 의미가 통하는 최소한의 오버로드 가능한 연산 집합을 지정한 다음, 인스턴스 암시적 인자를 갖는 다형 함수를 사용하여 이 오버로드된 연산을 기반으로 더 큰 기능 라이브러리를 제공합니다. 예를 들어, 함수 concat은 항목들이 이어붙이기 가능한 비어 있지 않은 리스트라면 어떤 것이든 이어붙일 수 있습니다:
def concat [Append α] (xs : NonEmptyList α) : α :=
let rec catList (start : α) : List α → α
| [] => start
| (z :: zs) => catList (start ++ z) zs
catList xs.head xs.tail하지만 일부 클래스의 경우, 데이터 타입 내부 구조에 대한 지식을 활용하면 더 효율적으로 구현할 수 있는 연산이 존재합니다.
이러한 경우에는 기본 메서드 정의를 제공할 수 있습니다. 기본 메서드 정의는 다른 메서드들을 이용하여 어떤 메서드의 기본 구현을 제공합니다. 하지만 인스턴스 구현자는 이 기본값을 더 효율적인 것으로 재정의할 수 있습니다. 기본 메서드 정의는 class 정의 안에 :=를 포함합니다.
Functor의 경우, 일부 타입은 매핑되는 함수가 자신의 인자를 무시할 때 map을 구현하는 더 효율적인 방법을 가지고 있습니다. 인자를 무시하는 함수는 항상 같은 값을 반환하기 때문에 상수 함수라고 불립니다. 다음은 Functor의 정의이며, 여기서 mapConst는 기본 구현을 갖습니다:
class Functor (f : Type → Type) where
map : {α β : Type} → (α → β) → f α → f β
mapConst {α β : Type} (x : α) (coll : f β) : f α :=
map (fun _ => x) coll
BEq를 준수하지 않는 Hashable 인스턴스가 버그인 것과 마찬가지로, 함수를 매핑하면서 데이터를 이리저리 옮기는 Functor 인스턴스 역시 버그입니다. 예를 들어, List에 대한 결함이 있는 Functor 인스턴스는 인자를 버리고 항상 빈 리스트를 반환하거나, 리스트를 뒤집을 수도 있습니다. PPoint에 대한 잘못된 Functor 인스턴스는 f x를 x와 y 필드 둘 다에 배치하거나, 이 둘을 뒤바꿀 수 있습니다. 구체적으로, Functor 인스턴스는 다음 두 가지 규칙을 따라야 합니다:
-
항등 함수를 매핑하면 원래의 인자가 결과로 나와야 합니다.
-
합성된 두 함수를 매핑하는 것은 각 함수의 매핑을 합성하는 것과 동일한 효과를 가져야 합니다.
더 형식적으로 말하면, 첫 번째 규칙은 id <$> x가 x와 같다는 것을 의미합니다. 두 번째 규칙은 map (fun y => f (g y)) x가 map f (map g x)와 같다는 것을 말합니다. 합성 f ∘ g는 fun y => f (g y)로도 쓸 수 있습니다. 이 규칙들은 데이터를 이리저리 옮기거나 일부를 삭제하는 방식으로 map을 구현하는 것을 방지합니다.
3.5.8. 만나게 될 수 있는 메시지
Lean은 모든 타입 클래스에 대해 인스턴스를 유도할 수 있는 것은 아닙니다. 예를 들어, 다음 코드는
deriving instance ToString for NonEmptyList다음과 같은 오류가 발생합니다:
deriving instance를 호출하면 Lean은 타입 클래스 인스턴스를 위한 코드 생성기의 내부 테이블을 참조합니다. 코드 생성기가 발견되면, 이를 주어진 타입에 대해 호출하여 인스턴스를 생성합니다. 하지만 이 메시지는 ToString에 대한 코드 생성기를 찾을 수 없었다는 것을 의미합니다.