まとめ
型クラスと構造体
型クラスは内部的には構造体として表現されます。クラスを定義することで対応する構造体が定義され、さらにインスタンスデータベースに空のテーブルが作成されます。インスタンスの定義によって構造体を型として持つか、その構造体を返す関数のどちらかの値が作成され、さらにテーブルにレコードが追加されます。インスタンス検索はインスタンステーブルを参照してインスタンスを構築します。構造体のクラスどちらでもフィールドのデフォルト値（メソッドの場合はデフォルト実装）を提供することができます。
構造体と継承
構造体はほかの構造体を継承することができます。その裏側では、他の構造体を継承した構造体は、元の構造体のインスタンスをフィールドとして含んでいます。言い換えると、継承は合成で実装されています。多重継承の場合、菱形継承問題を回避するために、親構造体に対して継承時に追加されたユニークなフィールドのみがその構造体のフィールドとして使用され、通常であれば親構造体の値を抽出する関数が、代わりに親の値を構築するために組み込まれます。レコードのドット記法は構造体の継承にも対応しています。
型クラスは単に構造体にいくつかの自動化が施されたものであるため、これらのすべての機能は型クラスで利用できます。デフォルトメソッドと組み合わせることで、きめ細かいインタフェースの階層を作ることができます。これはクライアントに実装にあたっての負荷を軽減します。というのも、大きなクラスが継承するデフォルトメソッドを含むような小さなクラスは自動的に実装されるからです。
アプリカティブ関手
アプリカティブ関手は関手に以下の2つの演算子を追加したものです：
pure、これはMonadの演算子と同じものですseqは関手のコンテキストのもとで関数をできるようにします
モナドが制御フローを持つ任意のプログラムを表現できるのに対し、アプリカティブ関手は関数の引数を左から右にしか実行できません。アプリカティブ関手はモナドほど強力ではないためインタフェースに反して書かれたプログラムをそこまで制御できませんが、その代わりにメソッドの実装の自由度が増します。いくつかの便利な型では Applicative を実装できる一方で Monad を実装することができません。
実は、型クラス Functor ・Applicative ・Monad は階層を構成しています。Functor から Monad へと階層が上がるにつれてより強力なプログラムを書けるようになりますが、より強力なクラスを実装できる型は限られてきます。多相なプログラムはできるだけ弱い抽象を使うように書くべきであり、データ型はできるだけ強力なインスタンスを与えるべきです。これはコードの再利用を最大化します。より強力な空クラスはより強力でない型を継承します。つまり、Monad の実装は Functor と Applicative の実装をタダで提供します。
各クラスには実装すべきメソッドの集合と、それに対応するメソッドに関する追加のルールを規定する約定があります。これらのインタフェースに対して書かれたプログラムは追加のルールが満たされていることを期待し、さもなければバグが発生する可能性があります。Functor のメソッドを Applicative のメソッドとして実装する場合、または Applicative のメソッドを Monad のメソッドとして実装する場合、デフォルトではこれらのルールに従います。
宇宙
Leanをプログラミング言語と定理証明器のどちらとしても使えるようにするためには、言語に対していくつかの制限が必要になります。これにはすべての再帰関数がちゃんと終了するか、partial とマークされ、空ではない型を返すことを保証するかのどちらかでなければならないという制限が含まれます。さらに、ある種の論理的なパラドックスを型として表現することは不可能でなければなりません。
このようなパラドックスを排除するための制約の1つに、すべての型が 宇宙 に割り当てられているというものがあります。宇宙とは Prop ・Type ・Type 1 ・Type 2 などの型のことです。これらの型はほかの型を記述します。ちょうど 0 と 17 が Nat によって記述されるように、Nat 自身が Type に、Type が Type 1 によって記述されます。型を引数に取る関数の型は引数の型よりも大きな宇宙でなければなりません。
宣言されたデータ型はそれぞれ宇宙を持つため、データ型をデータのように使うコードを書くとそれぞれの多相型を Type 1 から引数を取るようにコピペする必要があり、すぐに面倒なことになります。宇宙多相 と呼ばれる機能により、通常の多相でプログラムが型を引数としてとることができるように、Leanのプログラムとデータ型が宇宙レベルを引数として取ることができるようになります。一般的に、Leanにて多相的な操作のライブラリを実装する場合は宇宙多相を使うべきです。