まとめ

型クラスとオーバーロード

型クラスは、関数や演算子をオーバーロードするための機構です。多相関数は複数の型で使用できますが、どの型で使用しても同じように動作します。例えば、2つのリストを結合する多相関数は、リスト内の要素の型に関係なく使用できますが、どの型が見つかったかによって異なる動作をすることはできません。一方で、型クラスでオーバーロードされる演算もまた複数の型で使用することができます。しかし、それぞれの型はオーバーロードされた演算の独自の実装を必要とします。つまり、与えられた型によって動作が異なる可能性があります。

型クラス は名前とパラメータ、そしていくつかの名前と型からなる本体を持ちます。名前はオーバーロードされる演算を参照するためのもので、パラメータはオーバーロード可能な定義を決定し、そして本体はオーバーロードされる演算の名前と型シグネチャを提供します。オーバーロード可能な各演算は、型クラスの メソッド と呼ばれます。型クラスのいくつかのメソッドはほかのメソッドによるデフォルトの実装をされることもあり、実装者にとって必要がない場合はそれらを手で実装する必要はありません。

型クラスの インスタンス は、与えられたパラメータに対するメソッドの実装を提供します。インスタンスは多相的であることもあり。その場合はさまざまなパラメータに対して動作することができます。また、ある特定の型に対してより効率的なバージョンが存在する場合には、デフォルトメソッドのより具体的な実装を提供することもあります。

型クラスのパラメータは 入力パラメータ （デフォルト）か 出力パラメータ （ outParam 修飾子で示されます）のどちらかです。Leanはすべての入力パラメータがメタ変数でなくなるまでインスタンスの検索を開始しませんが、出力パラメータはインスタンスの検索中に解決することができます。型クラスのパラメータは型である必要ではなく、通常の値も可能です。自然数リテラルをオーバーロードするために使用される OfNat 型クラスは、オーバーロードされた Nat 自身をパラメータとして受け取り、これによりインスタンスにその数値を限定させることができます。

インスタンスには @[default_instance] 属性を付けることができます。インスタンス検索において型にメタ変数が存在してインスタンスを見つけることができない場合にはデフォルトインスタンスがフォールバックとして選択されます。

通常の文法に対しての型クラス

Leanのほとんどの中置演算子は型クラスでオーバーライドされています。例えば、加算演算子は Add という型クラスに対応しています。これらの演算子のほとんどには2つの引数が同じ型でなくても良い異なる型上の演算子が存在します。これらの異なる型上の演算子は HAdd のような H で始まるバージョンのクラスを使ってオーバーロードされます。

インデックス構文は GetElem という型クラスを使ってオーバーロードされます。GetElem には2つの出力パラメータがあり、コレクションから抽出される要素の型と、添え字の値がコレクションの範囲内にあることの根拠となるものを決定するために使用できる関数の2つです。この根拠は命題として記述され、インデックス記法が使用されると、Leanはこの命題の証明を試みます。Leanがコンパイル時にリストや配列のアクセス操作が境界内にあることをチェックできない場合、インデックス操作に ? を追加することでこのチェックを実行時に行うように遅延させることができます。

関手

関手とは、マッピング操作をサポートする多相型です。このマッピング操作は、すべての要素を「データ中のその位置で」変換し、ほかの構造は変更しません。例えば、リストは関手であり、マッピング操作はリスト内の要素を削除したり、重複させたり、並べ替えたりすることはできません。

関手は map を持つことで定義されますが、Leanの Functor 型クラスにはそれ以外にも、定数関数を値にマッピングするデフォルトメソッドが追加されており、多相型変数で与えられた型を持つすべての値を同じ新しい値で置き換えます。関手によっては、これは構造体全体を走査するよりも効率的に行うことができます。

インスタンスの導出

多くの型クラスはとても標準的な実装を持っています。例えば、真偽値の同値クラス BEq は通常、まず両方の引数が同じコンストラクタでビルドされているかどうかをチェックし、次にすべての引数が等しいかどうかをチェックすることで実装されています。これらのクラスのインスタンスは 自動的に 生成されます。

帰納型や構造体を定義するとき、宣言の最後に deriving 節を記述すると、自動的にインスタンスが生成されます。さらに deriving instance ... for ... コマンドをデータ型の定義の外側で使用すると、インスタンスを生成することができます。インスタンスを導出させることができるクラスはそれぞれ特別な処理を必要とするため、すべてのクラスが導出できるわけではありません。

型強制

期待された型と異なる型を指定した際に、通常であればコンパイル時にエラーとなるところを、Leanではある型から別の型にデータを変換する関数への呼び出しを挿入する型強制によってエラーを回避できます。例えば、任意の型 α から Option α 型への強制は、some コンストラクタではなく、値を直接書くことを可能にし、Option をオブジェクト指向言語のnullable型のように使うことができます。

強制には複数の種類があります。これらは異なる種類のエラーから回復することができ、それぞれの型クラスで表現されます。Coe クラスは型エラーを回復するために使われます。Leanが β 型を期待するコンテキストに α 型の式を置くと、Leanはまず α 型を β 型に変換できるような強制の連鎖を通そうと試み、それができなかった場合にのみエラーを表示します。CoeDep クラスは、強制される特定の値を追加パラメータとして受け取り、その値に対してさらに型クラスの検索を行うか、インスタンス内でコンストラクタを使用して変換の範囲を限定することができます。CoeFun クラスは、関数適用をコンパイルする際に「not a function」エラーとなるような値を途中で捕まえ、可能であれば関数の位置の値を実際の関数に変換できるようにします。