型クラスと多相性

与えられた関数の 任意の オーバーロードにおいて動作するような関数を書くと便利です。例えば、IO.println は ToString のインスタンスを持つすべての型に対して動作します。これを実現するには対象のインスタンスを角括弧で囲むことが必要とされ、実際に IO.println の型は {α : Type} → [ToString α] → α → IO Unit となっています。この型は IO.println が受け取る α 型の引数をLeanによって自動的に決定され、α に対して利用可能な ToString インスタンスがなければならないことを表しています。この関数は IO アクションを返します。

多相関数の型のチェック

暗黙の引数を取る関数や型クラスを使用する関数の型をチェックするにはいくつか追加の構文を利用する必要があります。単純に以下のように書くと

#check (IO.println)

メタ変数を伴った以下の型を出力します：

IO.println : ?m.3620 → IO Unit

Leanは暗黙の引数の発見に最善を尽くしますが、それでもメタ変数が存在するということから、暗黙の引数発見のために十分な型情報をまだ発見していないことを示しています。関数シグネチャを理解するために、関数名の前にアットマーク（ @ ）を付けてこの機能を抑制することができます：

#check @IO.println

@IO.println : {α : Type u_1} → [inst : ToString α] → α → IO Unit

この出力では、インスタンス自体に inst という名前が与えられています。さらに、Type の後に u_1 が続いていますが、これはまだ紹介していないLeanの機能を使用しています。今時点ではこれらの Type へのパラメータは無視してください。

暗黙のインスタンスを取る多相関数の定義

リストの要素をすべて足し合わせる関数は2つのインスタンスを必要とします：Add は要素を足すためのもので、0 に対する OfNat インスタンスは空のリストに対しての戻り値です：

def List.sum [Add α] [OfNat α 0] : List α → α
  | [] => 0
  | x :: xs => x + xs.sum

この関数は Nat のリストに対して使うことができます：

def fourNats : List Nat := [1, 2, 3, 4]

#eval fourNats.sum

しかし Pos の数値のリストに対しては使えません：

def fourPos : List Pos := [1, 2, 3, 4]

#eval fourPos.sum

failed to synthesize instance
  OfNat Pos 0

角括弧で囲まれた必須なインスタンスの指定は 暗黙のインスタンス （instance implicit）と呼ばれます。裏側では、すべての型クラスはオーバーロードされた演算ごとのフィールドを持つ構造体として定義されています。インスタンスはその構造体の値であり、各フィールドには具体的な実装が含まれています。呼び出し先では、Leanが各暗黙引数のインスタンスに渡す値を見つける責任を負います。通常の暗黙引数と暗黙のインスタンス引数の最も重要な違いは、Leanが引数の値を見つけるために使用する戦略です。通常の暗黙引数の場合、Leanは ユニフィケーション （unification）と呼ばれるテクニックを使って、プログラムが型チェッカをパスできるような一意の引数の値を見つけます。このプロセスは関数の定義と呼び出しにかかわる特定の型にのみ依存します。暗黙のインスタンスの場合、Leanはこの代わりにインスタンスの値についての組み込みテーブルを参照します。

Pos に対する OfNat のインスタンスが自然数 n を自動的な暗黙の引数として取っていたように、インスタンスもインスタンス自身の暗黙の引数を取ることができます。「多相性」節では、多相なポイント型を紹介しました：

structure PPoint (α : Type) where
  x : α
  y : α
deriving Repr

点の足し算を考える際には、その中にある x フィールドと y フィールド同士を足し算する必要があります。したがって、PPoint の Add インスタンスには、これらのフィールドの型がどういうものであってもそれ自体にも Add インスタンスが必要になります。言い換えると、PPoint の Add インスタンスには、さらに α の Add インスタンスが必要になります：

instance [Add α] : Add (PPoint α) where
  add p1 p2 := { x := p1.x + p2.x, y := p1.y + p2.y }

Leanが2つの点の足し算に遭遇すると、まずこのインスタンスを検索して見つけます。そして、Add α インスタンスをさらに検索します。

このようにして構築されるインスタンスの値は、型クラスの構造体型としての値です。再帰的なインスタンスの探索に成功すると、さらに別の構造体の値への参照を持つ構造体の値が得られます。Add (PPoint Nat) のインスタンスはこの過程で見つかった Add Nat のインスタンスへの参照を持ちます。

この再帰的な探索プロセスは、型クラスが単なるオーバーロードされた関数よりもはるかに大きなパワーを提供することを意味します。多相なインスタンスのライブラリは、コンパイラが独自に組み立てるコードを組むためのブロックの集合であり、必要な型以外は何も与えられていません。インスタンスを引数に取る多相関数は、型クラスの機構に対して、裏側で補助関数を組み立てるように潜在的に要求しています。APIのクライアントは、必要な部分をすべて手作業で組み立てる負担から解放されます。

メソッドと暗黙の引数

@OfNat.ofNat の型は意外に思われるかもしれません。これは {α : Type} → (n : Nat) → [OfNat α n] → α であり、Nat の引数 n は明示的な関数の引数として渡されます。しかし、メソッドの宣言においては ofNat は単に α 型を持ちます。このように一見矛盾しているように見えるのは、型クラスを宣言すると実際には以下のものが生成されるからです：

各オーバーロードされた演算の実装を持った構造体型
クラスと同じ名前の名前空間
各メソッドについて、インスタンスから実装を読んでくるためのクラスの名前空間にある関数

これは新しい構造体を宣言すると、アクセサ関数も宣言されるのと似ています。主な違いは、構造体のアクセサが構造体の値を明示的な引数として受け取るのに対し、型クラスのメソッドはインスタンスの値を暗黙のインスタンスとして受け取り、Leanが自動的に判定するようになっている点です。

Leanがインスタンスを見つけるためには、そのインスタンスの引数が利用可能でなければなりません。これは型クラスへの各引数が、メソッドの引数としてインスタンスの前に現れなければならないことを意味します。これらの引数を暗黙的にすると、Leanがその値を発見する作業を行ってくれるためとても便利です。例えば、@Add.add は {α : Type} → [Add α] → α → α → α という型を持っています。この場合、Add.add の引数がユーザが意図した型に関する情報を提供するため、型の引数 α は暗黙に指定することができます。この型を使用して Add インスタンスを検索することができます。

しかし ofNat の場合、デコードされる特定の Nat リテラルはほかの引数の一部として現れません。これは、仮にLeanが暗黙の引数 n を解釈しようとすると、使用する情報がないことを意味します。その結果、非常に不便なAPIになってしまいます。したがってこのような場合、Leanはクラスのメソッドに明示的な引数を使用します。

Functional Programming in Lean 日本語訳

型クラスと多相性

多相関数の型のチェック

暗黙のインスタンスを取る多相関数の定義

メソッドと暗黙の引数

演習問題

偶数値リテラル

再帰的なインスタンス探索の深さ