7. 型クラス（Type Classes）🔗

ある演算が多相（polymorphic）であるとは、それが複数の型で使用できることを指します。Lean では、多相性には3種類あります：

宇宙多相、これは定義中のソートを様々な方法でインスタンス化できることを指し、
型を（暗黙の可能性もある）パラメータとして受け取る関数、これによって1つのコードで任意の型に働きかけることができ、
アドホック多相性 （ad-hoc polymorphism）、これは型クラスによって実装されるもので、オーバーロードされる演算は型によって異なる演算を持つことができます。

Lean は型のケース分析を許容していないため、多相関数は任意に選んだ型引数に対して一様な演算を実装します；例えば、 List.map は、入力リストに String か Nat のどちらが含まれていようとも突然異なる計算をすることはありません。アドホック多相な演算は演算を実装するにあたって「一様な」方法がない場合に有益です；典型的な使用例としては、 Nat ・ Int ・ Float やその他加算の概念を持つ任意の型で動作するように算術演算子をオーバーロードすることです。アドホック多相は複数の型を含むこともあります；コレクション内の指定されたインデックスの値を検索するには、コレクション型・インデックス型・抽出されるメンバ要素の型が関係します。 型クラス型クラスが最初に記述されたのは Philip Wadler and Stephen Blott, 1980. “How to make ad-hoc polymorphism less ad hoc”. In Proceedings of the 16th Symposium on Principles of Programming Languages. です（type class）はオーバーロードされる演算（ メソッド 、method と呼ばれます）のコレクションを関連する型とともに記述します。

型クラスは非常に柔軟です。オーバーロードは複数の型に関係させることが可能です；データ構造へのインデックス付けのような操作は、データ構造・インデックス型・要素型・さらには構造体内のキーの存在を保証する述語の具体的な選択に対してまでもオーバーロードすることができます。Lean の表現力豊かな型システムにより、演算のオーバーロードは型だけに限定されません；型クラスは通常の値・型族・さらには述語や命題によってパラメータ化することができます。これらの可能性はすべて実際に使用されています：

自然数リテラル: OfNat 型クラスは自然数リテラルを解釈するために使用されます。インスタンスはインスタンス化される型だけでなく、数値リテラル自体にも依存します。

計算の作用: Monad のような型クラスはパラメータとしてある型から別の型の関数を取り、副作用を持つプログラムのための特別な構文を提供するために使用されます。具体的には、操作がオーバーロードされる「型」は Option ・ IO ・ Except などの型レベルの関数です。

述語と命題: Decidable 型クラスによって Lean が命題の決定手続きを自動的に見つけることができるようにします。これは決定可能な任意の命題への分岐を可能にする termIfThenElse : term`if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to return `t` or `e` depending on whether `c` is true or false. The explicit argument `c : Prop` does not have any actual computational content, but there is an additional `[Decidable c]` argument synthesized by typeclass inference which actually determines how to evaluate `c` to true or false. Write `if h : c then t else e` instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact that `c` is true/false.if 式の基礎として使われています。

通常の多相定義は単に任意のパラメータでインスタンス化されることを想定していますが、型クラスでオーバーロードされる演算子は特定のパラメータセットに対してオーバーロードされる演算を定義する インスタンス （instance）としてインスタンス化されます。これらのインスタンス暗黙（instance-implicit）パラメータは大括弧で示されます。呼び出しの際において、Lean は利用可能な候補から適切なインスタンスを統合（synthesize）するかエラーを通知します。インスタンスはそれ自身がインスタンスパラメータを持つことがあるため、この検索プロセスは再帰的であり、様々なインスタンスからのコードを組み合わせた最終的な合成インスタンス値になる可能性があります。このように型クラスのインスタンス統合は型指向の流儀によるプログラムを構築する手段でもあります。

ここでいくつか型クラスの一般的な使用例を挙げましょう：

型クラスはオーバーロードされた演算子を表すことができ、それは例えば様々な型の数値に使用できる算術演算や、様々なデータ構造に使用できるメンバシップ述語などです。演算子はそれぞれの型に対して標準的なものが1つだけ存在することがしばしばあります。結局のところ、 Nat の加算に対して感覚的な代替定義は存在しないものの、これは本質的な性質ではないため、必要であればライブラリは別のインスタンスを提供することが可能です。
型クラスは代数的構造を表現することができ、その構造で必要とされる追加の構造と公理の両方を提供します。例えば、アーベル群を表す型クラスには二項演算子・単項逆演算子・単位元のメソッドと、二項演算子が結合的かつ可換であること・この単位元が実際に単位であること・逆演算子を演算子の左右どちらにおいても単位元をもたらすことの証明を含ませることができます。ここで、こうした構造に対する標準的な選択は存在しないかもしれず、ライブラリはある公理のセットに対してインスタンス化する方法を多数提供するかもしれません；例えば整数上には2つの標準的なモノイド構造があります。
型クラスは2つの型の間の関係を表すことができ、ライブラリによって2つの型を一緒に使うことができます。 Coe クラスはある型から別の型へ自動的に挿入される強制子を表し、 MonadLift はある種の作用を持つ操作を別の種類の作用を期待するコンテキストで実行する方法を表します。
型クラスは型駆動コード生成のフレームワークを表すことができ、多相型のインスタンスはそれぞれ最終的なプログラムの一部に貢献します。 Repr クラスは型のための標準的なプリティプリンタを定義し、多相型の場合は多相型用の Repr インスタンスに行きつきます。最終的にプリティプリンタが List (Nat × (String ⊕ Int)) のような既知の具体的な型を持つ式に対して呼び出されると、結果として得られるプリティプリンタには List ・ Prod ・ Nat ・ Sum ・ String ・ Int の Repr インスタンスから組み立てられたコードが含まれます。