3.5. Standard Classes🔗

이 절에서는 Lean의 타입 클래스로 오버로딩할 수 있는 다양한 연산자와 함수를 소개한다. 각 연산자와 함수는 타입 클래스의 메서드에 대응한다. C++와 달리 Lean의 중위 연산자는 이름 있는 함수의 약어로 정의되므로, 새 타입에서 오버로딩할 때 연산자 자체가 아니라 내부 이름(예: HAdd.hAdd)을 사용한다.

3.5.1. Arithmetic🔗

대부분의 산술 연산자는 인수 타입이 달라도 되고 출력 매개변수가 결과 표현식의 타입을 결정하는 이종 형태로 제공된다. 각 이종 연산자에는 이름에서 h를 뺀 동종 버전이 대응한다. 예를 들어 HAdd.hAdd는 Add.add가 된다. 다음 산술 연산자가 오버로딩된다.

표현식	구문 해석	클래스 이름
`x + y`	`HAdd.hAdd x y`	`HAdd`
`x - y`	`HSub.hSub x y`	`HSub`
`x * y`	`HMul.hMul x y`	`HMul`
`x / y`	`HDiv.hDiv x y`	`HDiv`
`x % y`	`HMod.hMod x y`	`HMod`
`x ^ y`	`HPow.hPow x y`	`HPow`
`- x`	`Neg.neg x`	`Neg`

3.5.2. Bitwise Operators🔗

Lean에는 타입 클래스로 오버로딩된 표준 비트 연산자가 여러 개 있다. UInt8, UInt16, UInt32, UInt64, USize 같은 고정 폭 타입에 인스턴스가 있다. 마지막 타입은 현재 플랫폼의 워드 크기이며 보통 32비트나 64비트다. 다음 비트 연산자가 오버로딩된다.

표현식	구문 해석	클래스 이름
`x &&& y`	`HAnd.hAnd x y`	`HAnd`
`x \|\|\| y`	`HOr.hOr x y`	`HOr`
`x ^^^ y`	`HXor.hXor x y`	`HXor`
`~~~x`	`Complement.complement x`	`Complement`
`x >>> y`	`HShiftRight.hShiftRight x y`	`HShiftRight`
`x <<< y`	`HShiftLeft.hShiftLeft x y`	`HShiftLeft`

And와 Or가 논리 연결사의 이름으로 이미 사용되므로 HAnd와 HOr의 동종 버전은 And, Or 대신 AndOp, OrOp라 부른다.

3.5.3. Equality and Ordering🔗

두 값의 동등성 검사는 보통 “불리언 동등성”의 약자인 BEq 클래스를 사용한다. Lean을 정리 증명기로도 사용하기 때문에 Lean에는 실제로 두 종류의 동등성 연산자가 있다.

불리언 동등성은 다른 프로그래밍 언어의 동등성과 같다. 두 값을 받아 Bool을 반환하는 함수다. 불리언 동등성은 Python과 C#처럼 등호 두 개로 쓴다. Lean은 순수 함수형 언어이므로 참조 동등성과 값 동등성을 따로 구분하지 않으며 포인터를 직접 관찰할 수 없다.
명제적 동등성은 두 대상이 같다는 수학적 진술이다. 명제적 동등성은 함수가 아니라 증명을 허용하는 수학적 진술이며 등호 하나로 쓴다. 명제적 동등성 진술은 이 동등성의 증거를 분류하는 타입과 같다.

두 동등성 개념은 모두 중요하며 서로 다른 목적에 사용된다. 불리언 동등성은 두 값이 같은지 결정해야 하는 프로그램에서 유용하다. 예를 들어 "Octopus" == "Cuttlefish"는 false로, "Octopodes" == "Octo".append "podes"는 true로 평가된다. 함수처럼 일부 값은 동등성을 검사할 수 없다. 예를 들어 (fun (x : Nat) => 1 + x) == (Nat.succ ·)는 다음 오류를 낸다.

failed to synthesize instance of type class
  BEq (Nat → Nat)

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

이 메시지가 보여 주듯 ==는 타입 클래스로 오버로딩된다. 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는 명제다.

2 < 4 : Prop#check 2 < 4

2 < 4 : Prop

그럼에도 이를 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"는 다음 결과를 낸다.

failed to synthesize instance of type class
  Decidable ((fun x => 1 + x) = fun x => x.succ)

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

보통 결정 가능한 다음 명제는 타입 클래스로 오버로딩된다.

표현식	구문 해석	클래스 이름
`x < y`	`LT.lt x y`	`LT`
`x ≤ y`	`LE.le x y`	`LE`
`x > y`	`LT.lt y x`	`LT`
`x ≥ y`	`LE.le y x`	`LE`

새 명제를 정의하는 방법은 아직 보이지 않았으므로 완전히 새로운 LT, LE 인스턴스를 정의하기는 어려울 수 있다. 그러나 기존 인스턴스로 정의할 수 있다. Pos의 LT, LE 인스턴스는 Nat의 기존 인스턴스를 사용할 수 있다.

instance : LT Pos where
  lt x y := LT.lt x.toNat y.toNat

instance : 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) :=
  Type mismatch
  inferInstance
has type
  Decidable (x.toNat < y.toNat)
but is expected to have type
  Decidable (x ≤ y)(inferInstance : Decidable (x.toNat < y.toNat))

Type mismatch
  inferInstance
has type
  Decidable (x.toNat < y.toNat)
but is expected to have type
  Decidable (x ≤ y)

<, ==, >로 값을 비교하면 비효율적일 수 있다. 한 값이 다른 값보다 작은지 확인한 뒤 같은지도 확인하려면 큰 데이터 구조를 두 번 순회해야 할 수 있다. 이 문제를 해결하기 위해 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. Hashing🔗

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 := hashBinTree

3.5.5. Deriving Standard Classes🔗

BEq, Hashable 같은 클래스의 인스턴스는 손으로 구현하면 대개 매우 번거롭다. Lean에는 컴파일러가 많은 타입 클래스의 올바른 인스턴스를 자동으로 구성하게 하는 인스턴스 유도 기능이 있다. 실제로 다형성 첫 절의 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

적어도 다음 클래스의 인스턴스를 유도할 수 있다.

Inhabited
BEq
Repr
Hashable
Ord

그러나 어떤 경우에는 유도된 Ord 인스턴스가 응용에서 원하는 순서를 정확히 만들지 못할 수 있다. 그럴 때는 Ord 인스턴스를 직접 작성해도 된다. 고급 Lean 사용자는 인스턴스를 유도할 수 있는 클래스의 모음을 확장할 수 있다.

프로그래머 생산성과 코드 가독성이 향상될 뿐 아니라, 타입 정의가 바뀔 때 인스턴스도 갱신되므로 인스턴스 유도는 코드 유지 관리도 쉽게 한다. 코드 변경을 검토할 때 데이터 타입을 갱신하는 변경은 동등성 검사와 해시 계산을 형식적으로 한 줄씩 수정하지 않아도 되어 훨씬 읽기 쉽다.

3.5.6. Appending🔗

많은 데이터 타입에는 값을 이어 붙이는 연산자가 있다. Lean에서는 산술 연산과 같은 이종 연산인 HAppend 타입 클래스로 두 값을 이어 붙이는 연산을 오버로딩한다.

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 }

위 인스턴스를 정의한 뒤

{ head := "Banded Garden Spider",
  tail := ["Long-legged Sac Spider",
           "Wolf Spider",
           "Hobo Spider",
           "Cat-faced Spider",
           "Banded Garden Spider",
           "Long-legged Sac Spider",
           "Wolf Spider",
           "Hobo Spider",
           "Cat-faced Spider"] }#eval idahoSpiders ++ idahoSpiders

다음 출력이 나온다.

{ head := "Banded Garden Spider",
  tail := ["Long-legged Sac Spider",
           "Wolf Spider",
           "Hobo Spider",
           "Cat-faced Spider",
           "Banded Garden Spider",
           "Long-legged Sac Spider",
           "Wolf Spider",
           "Hobo Spider",
           "Cat-faced Spider"] }

마찬가지로 HAppend를 정의하면 비어 있지 않은 리스트를 일반 리스트에 이어 붙일 수 있다.

instance : HAppend (NonEmptyList α) (List α) (NonEmptyList α) where
  hAppend xs ys :=
    { head := xs.head, tail := xs.tail ++ ys }

이 인스턴스가 있으면

{ head := "Banded Garden Spider",
  tail := ["Long-legged Sac Spider", "Wolf Spider", "Hobo Spider", "Cat-faced Spider", "Trapdoor Spider"] }#eval idahoSpiders ++ ["Trapdoor Spider"]

다음 결과가 나온다.

{ head := "Banded Garden Spider",
  tail := ["Long-legged Sac Spider", "Wolf Spider", "Hobo Spider", "Cat-faced Spider", "Trapdoor Spider"] }

3.5.7. Functors🔗

다형 타입이 내부의 모든 원소를 함수로 변환하는 map 함수의 오버로딩을 가지면 Functor다. 대부분의 언어가 이 용어를 사용하지만 C#에서 map에 대응하는 것은 System.Linq.Enumerable.Select다. 예를 들어 리스트에 함수를 매핑하면 각 원소를 함수 결과로 바꾼 새 리스트가 만들어진다. Option에 함수 f를 매핑하면 none은 그대로 두고 some x를 some (f x)로 바꾼다.

다음은 Functor와 그 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 버전을 만들 수 있겠지만, Functor의 일부는 map이 어떤 원소 타입에서도 동작한다는 것이다.

PPoint의 Functor 인스턴스는 다음과 같다.

instance : Functor PPoint where
  map f p := { x := f p.x, y := f p.y }

이 경우 f가 x와 y 모두에 적용된다.

Functor 안의 타입 자체가 Functor여도 함수 매핑은 한 계층만 내려간다. 즉 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을 더 효율적으로 구현할 수 있다. 인수를 무시하는 함수는 항상 같은 값을 반환하므로 상수 함수라 부른다. 다음은 mapConst에 기본 구현을 제공하는 Functor 정의다.

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. Messages You May Meet🔗

Lean은 모든 클래스의 인스턴스를 유도할 수 없다. 예를 들어 다음 코드는

deriving instance No deriving handlers have been implemented for class `ToString`ToString for NonEmptyList

다음 오류를 낸다.

No deriving handlers have been implemented for class `ToString`

deriving instance를 호출하면 Lean은 타입 클래스 인스턴스 코드 생성기 내부 테이블을 참조한다. 코드 생성기를 찾으면 제공된 타입에 적용해 인스턴스를 만든다. 하지만 이 메시지는 ToString용 코드 생성기를 찾지 못했다는 뜻이다.

3.5.9. Exercises🔗

HAppend (List α) (NonEmptyList α) (NonEmptyList α) 인스턴스를 작성하고 테스트하라.
이진 트리 데이터 타입의 Functor 인스턴스를 구현하라.