3.5. 표준 클래스
이 절에서는 Lean에서 타입 클래스를 사용해 오버로딩할 수 있는 다양한 연산자와 함수를 소개합니다. 각 연산자나 함수는 타입 클래스의 메서드 하나에 대응합니다. C++와 달리 Lean의 중위 연산자는 이름이 있는 함수의 약어로 정의됩니다. 따라서 새로운 타입에 대해 중위 연산자를 오버로딩할 때는 연산자 자체가 아니라 그 바탕이 되는 이름(HAdd.hAdd 등)을 사용합니다.
3.5.1. 산술
대부분의 산술 연산자는 이종(heterogeneous) 형태로도 제공됩니다. 이 형태에서는 인자들의 타입이 서로 다를 수 있으며, 출력 매개변수가 결과 표현식의 타입을 결정합니다. 각 이종 연산자에는 대응하는 동종(homogeneous) 버전이 있으며, 이는 글자 h를 제거하면 찾을 수 있습니다. 예를 들어 HAdd.hAdd는 Add.add가 됩니다. 다음 산술 연산자들이 오버로드되어 있습니다.
표현식 | 디슈거링 | 클래스 이름 |
|---|---|---|
|
| |
|
| |
|
| |
|
| |
|
| |
|
| |
|
|
3.5.2. 비트 연산자
Lean에는 타입 클래스를 사용해 오버로드된 여러 표준 비트 연산자가 있습니다. UInt8, UInt16, UInt32, UInt64, USize와 같은 고정 폭 타입에 대한 인스턴스가 있습니다. 마지막 타입은 현재 플랫폼의 워드 크기로, 일반적으로 32비트 또는 64비트입니다. 다음 비트 연산자가 오버로드되어 있습니다.
표현식 | 디슈거링 | 클래스 이름 |
|---|---|---|
|
| |
|
| |
|
| |
|
|
|
| ||
|
And와 Or라는 이름은 이미 논리 연결사의 이름으로 쓰이고 있으므로, HAnd와 HOr의 동종 버전은 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라는 점에서 알 수 있듯이, 이 둘의 차이는 때때로 흐려집니다. 어떤 명제는 결정 가능합니다. 이는 불리언 함수처럼 검사할 수 있다는 뜻입니다. 명제가 참인지 거짓인지를 검사하는 함수를 결정 절차라고 하며, 이 함수는 명제가 참인지 거짓인지에 대한 증거를 반환합니다. 결정 가능한 명제의 예로는 자연수의 같음과 다름, 문자열의 같음, 그리고 그 자체로 결정 가능한 명제들의 “그리고”와 “또는”이 있습니다.
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와 다른 것은 아니지만(어차피 Nat 값은 UInt64 값보다 무한히 많습니다), 서로 다른 값이 서로 다른 해시를 가질 가능성이 높을수록 해싱을 기반으로 만든 자료 구조의 성능이 더 좋아집니다. 이는 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. 이어붙이기
많은 데이터 타입에는 일종의 이어 붙이기 연산자가 있습니다. Lean에서 두 값을 이어 붙이는 연산은 타입 클래스 HAppend로 오버로드되며, 이는 산술 연산에 사용되는 것과 같은 이종(heterogeneous) 연산입니다:
class HAppend (α : Type) (β : Type) (γ : outParam Type) where
hAppend : α → β → γ
xs ++ ys 문법은 HAppend.hAppend xs ys로 디슈거링됩니다. 두 타입이 같은 경우에는 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
Hashable 인스턴스가 BEq를 따르지 않으면 버그인 것과 마찬가지로, 함수를 매핑하면서 데이터의 위치를 옮기는 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에 대한 코드 생성기를 찾지 못했다는 뜻입니다.