標準クラス

この節では、Leanの型クラスを使ってオーバーロードできるさまざまな演算子や関数を紹介します。各演算子や関数は型クラスのメソッドに対応します。C++とは異なり、Leanの中置演算子は名前のある関数の省略形として定義されています：これの意味するところは、新しい型に対する演算子のオーバーロードは演算子そのものによる処理ではなく、その裏側にある名前（例えば HAdd.hAdd ）を使って行っているということです。

算術演算

ほとんどの算術演算子は異なる型上の演算子として利用可能で、引数の型が異なる場合があり、また出力パラメータがその演算結果の型を決定します。各異なる型上の演算子それぞれに、型クラスとメソッドから h を取り除いた同じ型上の演算子が存在します。例えば HAdd.hAdd に対応するものとして、Add.add が定義されています。Leanでは以下の算術演算子がオーバーロードされています：

ビット演算子

Leanには型クラスを使用してオーバーロードされる標準のビット演算子がたくさんあります。例えば固定幅の型に対するインスタンスとして、UInt8 や UInt16 、UInt32 、UInt64 、USize などがあります。最後のものは実行環境の1文字に対応するサイズで、通常は32ビットか64ビットです。以下のビット演算子がオーバーロードされています：

同じ型上の演算子について、And と Or という名前は論理結合子としてもうすでに取られてしまっているため、同じ型上の演算子バージョンの HAnd と HOr はそれぞれ AndOp と OrOp と名付けられています。

同値と順序

2つの値の同値性を評価するには、通常 BEq クラスを使用します。これは「Boolan equality」の省略形です。Leanは定理証明器として使用されるため、Leanには2種類の同値演算子が存在します：

• 真偽値の同値 （Boolean equality）は他のプログラミング言語にも存在する等号と同じです。これは2つの値を取り、Bool 値を返す関数です。PythonやC#と同じように、真偽値の同値は等号を2つ用いて書かれます。Leanは純粋な関数型言語であるため、参照の同値と値の同値という個別の概念はありません。ポインタの中身は直接見ることができません。
• 命題の同値 （Propositional equality）は2つのものが等しいということの数学的な文です。命題の同値は関数ではありません；むしろ証明可能な数学的な文です。これは等号を1つ使って記述されます。命題の同値の文は、この等式の根拠を分類する型のようなものです。

これらの等号の概念はどちらも重要であり、それぞれ異なる目的で用いられます。ある判断が2つの値が等しいかどうかということから構成される必要がある場合、そのプログラムでは真偽値の同値が有効です。例えば、"Octopus" == "Cuttlefish" は false と評価され、"Octopodes" == "Octo".append "podes" は true と評価されます。一方で関数のようないくつかの値については等しいかどうかのチェックができません。例えば (fun (x : Nat) => 1 + x) == (Nat.succ ·) は以下のエラーを出力します：

failed to synthesize instance
  BEq (Nat → Nat)

このメッセージが示している通り、== は型クラスによるオーバーロードされた演算子です。そのため、式 x == y は実際には BEq.beq x y の省略形です。

命題の同値はプログラムの呼び出しではなく、数学的な文です。命題はある文の根拠を記述する型のようなものであるため、真偽値の同値よりも String や Nat → List Int などのような型との共通点が多いです。このため、この同値は自動的にチェックすることができません。しかし、2つの式の同値性は、その2つが同じ型である限りLeanで記述することはできます。したがって (fun (x : Nat) => 1 + x) = (Nat.succ ·) は文として完全に妥当に成立しています。数学の観点において、2つの関数が同値であるとは同じ入力から同じ出力に写す場合のことであるため、先ほどの文は真となります。にもかかわらずこの事実をLeanに納得させるためには2行の証明が必要になります。

一般的に、Leanを定理証明器ではなくプログラミング言語として用いる場合には命題よりも真偽値の関数に頼るほうが非常に容易です。しかし、Bool のコンストラクタに true と false という名前が付けられているため、この違いは時として曖昧です。またいくつかの命題はブール関数と同じようにチェックすることができ、これを 決定可能 （decidable）と呼びます。命題が真か偽かをチェックする関数は 決定手続き （decision procedure）と呼ばれ、命題の真偽の 根拠 を返します。決定可能な命題の例としては、自然数か文字列の等式と不等式、そしてそれ自体が決定可能な命題同士を「かつ」と「または」で組み合わせたものなどがあります。

Leanでは、if は決定可能な命題と組み合わせることができます。例えば、2 < 4 は以下のように命題になります：

#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
  Decidable ((fun x => 1 + x) = fun x => Nat.succ x)

以下の命題（通常は決定可能である）はそれぞれ下記の型クラスでオーバーロードされています：

新しい命題の定義の仕方についてはまだ披露していないため、LT と LE の新しいインスタンスを定義するのは難しいかもしれません。

ところで、< と == 、>を使った値の比較は効率的ではありません。ある値が別の値未満かどうかをチェックし、次にそれらが等しいかどうかのチェックをするとなると、同じデータ全体を2回走査する必要があり、大きなデータ構造では時間がかかってしまいます。この問題を解決するために、JavaとC#には標準でそれぞれ compareTo と CompareTo メソッドがあり、これをクラスでオーバーライドすることで、3つの操作を同時に実装することができます。これらのメソッドは、受け取るオブジェクトが引数未満の場合は負の整数を返し、等しい場合は0を返し、引数より大きい場合は正の整数を返します。Leanではこのように整数を使った手法のオーバーロードではなく、これら3つのケースを記述する組み込みの帰納型を持っています：

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

Leanにおいて、Javaでの compareTo のアプローチが有効であるようなシチュエーションでは、Ord.compare を使いましょう。

ハッシュ化

JavaとC#ではそれぞれ hashCode と GetHashCode メソッドを有しており、ハッシュテーブルのようなデータ構造で使用する値のハッシュを計算します。Leanにおいて Hashale 型クラスがこれに相当します：

class Hashable (α : Type) where
  hash : α → UInt64

もし2つの値がその型の 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 := hashBinTree

標準の型クラスの自動的な導出

BEq や Hashable のようなクラスのインスタンスを手作業で実装するのは非常に面倒です。Leanには インスタンス導出 （instance deriving）と呼ばれる機能があり、コンパイラが自動的に多くの型クラスに対して行儀のよい（well-behaved）インスタンスを構築することができます。実は、「構造体」節 の Point の定義にある deriving Repr というフレーズはインスタンス導出の一例です。

インスタンスは2つの方法で導出することができます。1つ目は構造体や帰納型を定義する時です。この場合、型宣言の最後に deriving を追加し、その後にインスタンスを導出させるクラスの名前を追加します。すでに定義されている型の場合は、単独の deriving コマンドを使用することができます。deriving instance C1, C2, ... for T と書くことで、T 型に対して C1, C2, ... のインスタンスを後から導出させることができます。

Pos と NonEmptyList に対しての BEq と Hashable のインスタンスは非常に少ないコード量で導出することができます：

deriving instance BEq, Hashable for Pos
deriving instance BEq, Hashable, Repr for NonEmptyList

このほか、例えば以下のクラスに対してもインスタンスの導出が可能です：

• Inhabited
• BEq
• Repr
• Hashable
• Ord

しかし場合によっては、Ord インスタンスの導出がアプリケーションで必要とされる順序とならないことがあります。このような場合では、手作業で Ord インスタンスを書いても問題はありません。インスタンスを導出させることができるクラスのコレクションの拡張はLeanに精通したユーザでないと難しいでしょう。

プログラマの生産性とコードの可読性という明確な利点のほかに、インスタンスの導出はコードの保守を容易にします。なぜなら導出されたインスタンスは型の定義に付随して更新されるからです。データ型の更新を伴う変更セットは、同値テストやハッシュ計算について各行ごとに形式的な修正をいちいちする必要がなく、読みやすくなります。

結合

多くのデータ型には、ある種のデータの結合のための演算子があります。Leanにおいて2つの値の結合は 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 }

上記のインスタンスを定義することで：

#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 }

このインスタンスによって以下が可能になり、

#eval idahoSpiders ++ ["Trapdoor Spider"]

以下の出力になります。

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

関手

多相型 関手 （functor）とは、その型に格納されているすべての要素を何かしらの関数で変換する map という名前の関数のオーバーロードを持ちます。ほとんどの言語でこの用語が使われており、例えばC#では System.Linq.Enumerable.Select と呼ばれるものがこの map に相当します。例えば、関数 f をリスト全体にマッピングすると、入力のリストの各要素がその関数の結果で置き換えられた新しいリストが作成されます。関数 f を Option にマッピングすると、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 }

ここで、後続のリストに対しては List に対する Functor インスタンスの map を使用してマッピングしています。このインスタンスは 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 の両方に適用されます。

関手に含まれる型自体が関手である場合でも、関数のマッピングは1つ下の階層にしか行きません。つまり、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 の実装方法を持つ型があります。引数を無視する関数は常に同じ値を返すので、 定数関数 （constant function）と呼ばれます。以下は 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 のまずいインスタンスは x と y の両方のフィールドに f x を置いたりするものもあるでしょう。具体的には、Functor インスタンスは次の2つのルールに従う必要があります：

1. 恒等関数のマッピングはもともとの引数をそのまま返さなければならない。
2. 2つの関数を合成した関数のマッピングはそれぞれをマッピングしたものを合成したものと同じ作用を持たなければならない。

より正式には、最初のルールは id <$> x が x に等しいことを指します。2番目のルールは map (fun y => f (g y)) x が map f (map g x) に等しいことを述べています。合成 fun y => f (g y) は f ∘ g とも書くことができます。これらのルールは map の実装がデータを移動したり、一部を削除したりしてしまうことを防ぎます。

見るかもしれないメッセージ

Leanはすべてのクラスのインスタンスを導出させることはできません。例えば、次のコードは

deriving instance ToString for NonEmptyList

以下のエラーを引き起こします：

default handlers have not been implemented yet, class: 'ToString' types: [NonEmptyList]

deriving instance を呼び出すと、Leanは型クラスのインスタンスに対するコードジェネレータの内部テーブルを参照します。もし対応するコードジェネレータが見つかれば、インスタンスを生成するために指定された型に対してそのコードジェネレータが呼び出されます。しかし、このメッセージは ToString のコードジェネレータが見つからなかったことを意味します。

演習問題

• HAppend (List α) (NonEmptyList α) (NonEmptyList α) のインスタンスを記述し、動作を確認してください。
• 二分木のデータ型に対して Functor インスタンスを実装してください。