構造体と継承
Functor と Applicative 、Monad の完全な定義を理解するためには、構造体の継承というLeanの機能が必要になります。構造体の継承は、ある構造体型にフィールドを追加した別の構造体のインタフェースを提供することを可能にします。これは明確な分類学的な関係を持つ概念をモデル化するときに便利です。例えば、神話上の生き物のモデルを考えてみましょう。その中には大きいものも居れば、小さいものも居ます：
structure MythicalCreature where
large : Bool
deriving Repr
裏側では、MythicalCreature 構造体を定義すると mk というコンストラクタを1つだけ持つ帰納型が作られます：
#check MythicalCreature.mk
MythicalCreature.mk (large : Bool) : MythicalCreature
同様に、コンストラクタから実際のフィールドを取り出す関数 MythicalCreature.large が作られます：
#check MythicalCreature.large
MythicalCreature.large (self : MythicalCreature) : Bool
ほとんどの昔話において、それぞれの怪物は何らかの方法で倒すことができます。怪物の説明文には、大型かどうかと共に、この情報を含めるべきでしょう：
structure Monster extends MythicalCreature where
vulnerability : String
deriving Repr
先頭行に含まれる extends MythicalCreature はすべての怪物もまた神話的であると述べています。Monster を定義するには、MythicalCreature のフィールドと Monster のフィールドの両方を提供しなければなりません。トロールは大型の怪物で、その弱点は日光です：
def troll : Monster where
large := true
vulnerability := "sunlight"
裏側では、継承は合成を用いて実装されています。コンストラクタ Monster.mk は MythicalCreature を引数に取ります：
#check Monster.mk
Monster.mk (toMythicalCreature : MythicalCreature) (vulnerability : String) : Monster
各新しいフィールドの値を抽出する関数の定義に加えて、Monster → MythicalCreature 型の関数 Monster.toMythicalCreature が定義されています。これはベースになっている生き物を抽出するために使用できます。
Leanにおける継承の階層の移動はオブジェクト指向言語におけるアップキャストとは異なります。アップキャスト演算子は派生クラスの値を親クラスのインスタンスとして扱いますが、値自体は中身も構造もそのままです。しかしLeanでは、継承階層を上がることで実際にその中に含まれる情報を削除します。このことを実際に見るために、troll.toMythicalCreature の評価結果を考察してみましょう：
#eval troll.toMythicalCreature
{ large := true }
MythicalCreature のフィールドだけが残ります。
where 構文と同様に、フィールド名を伴った波括弧記法でも構造体の継承が機能します：
def troll : Monster := {large := true, vulnerability := "sunlight"}
その一方で、基礎となるコンストラクタに委譲する無名の角括弧記法では内部構造があらわになります：
def troll : Monster := ⟨true, "sunlight"⟩
application type mismatch
Monster.mk true
argument
true
has type
Bool : Type
but is expected to have type
MythicalCreature : Type
ここでは true で MythicalCreature.mk が起動するようにもう1つ角括弧が必要になります：
def troll : Monster := ⟨⟨true⟩, "sunlight"⟩
Leanのドット記法は継承を考慮にいれることを許容しています。言い換えると、既存の MythicalCreature.large は Monster で使用することができ、その際にはLeanが自動的に MythicalCreature.large の呼び出し前に Monster.toMythicalCreature の呼び出しを挿入します。しかしこれはドット記法を使った場合のみに発生し、通常の関数呼び出し構文を使用してフィールド検索関数を適用すると型エラーが発生します：
#eval MythicalCreature.large troll
application type mismatch
troll.large
argument
troll
has type
Monster : Type
but is expected to have type
MythicalCreature : Type
ドット記法はユーザ定義関数に対しても継承を考慮にいれることができます。小さい生き物とは、大きくない生き物のことです：
def MythicalCreature.small (c : MythicalCreature) : Bool := !c.large
troll.small を評価すると false が出力される一方で、MythicalCreature.small troll は評価しようとすると以下の結果になります：
application type mismatch
MythicalCreature.small troll
argument
troll
has type
Monster : Type
but is expected to have type
MythicalCreature : Type
多重継承
ヘルパーとは神話上の生き物で、適切な報酬が与えられれば援助を提供してくれます：
structure Helper extends MythicalCreature where
assistance : String
payment : String
deriving Repr
例えば、ニッセ は小さな妖精の一種で、おいしいおかゆをあげると家の手伝いをしてくれると言われています：
def nisse : Helper where
large := false
assistance := "household tasks"
payment := "porridge"
もし従えることができれば、トロールは優秀なヘルパーになります。トロールは畑一面をすべて耕すのに1晩でできるほどパワフルですが、彼らの生活を満足させるためにはヤギの模型が必要です。怪物のような助っ人は、ヘルパーでもある怪物のことです：
structure MonstrousAssistant extends Monster, Helper where
deriving Repr
この構造体型の値は、親である両方の構造体のフィールドをすべて埋めなければなりません：
def domesticatedTroll : MonstrousAssistant where
large := false
assistance := "heavy labor"
payment := "toy goats"
vulnerability := "sunlight"
どちらの親構造体型も MythicalCreature を継承しています。もし単純に多重継承を実装しようとすると、large を MonstrousAssistant から取得する際の経路が不明確になるという「菱形継承問題」が発生する可能性があります。large は含まれている Monster と、それとも Helper のどちらから取るべきしょうか？Leanでは、新しい構造体が両方の親を直接含むのではなく、最初に指定された親の親構造体へのパスが取得され、そののちに親構造で追加されたフィールドがコピーされるという解決策を取っています。
これは MonstrousAssistant のコンストラクタのシグネチャを調べればわかります：
#check MonstrousAssistant.mk
MonstrousAssistant.mk (toMonster : Monster) (assistance payment : String) : MonstrousAssistant
このコンストラクタは Monster と、MythicalCreature に Helper で導入されている2つのフィールドを引数に取ります。同じように、MonstrousAssistant.toMonster はコンストラクタからただ Monster を取り出すだけですが、MonstrousAssistant.toHelper には取り出せる Helper がありません。#print コマンドからこの実装を明らかにすることができます：
#print MonstrousAssistant.toHelper
@[reducible] def MonstrousAssistant.toHelper : MonstrousAssistant → Helper :=
fun self =>
{ toMythicalCreature := self.toMonster.toMythicalCreature, assistance := self.assistance, payment := self.payment }
この関数は MonstrousAssistant のフィールドから Helper を作成しています。@[reducible] 属性は abbrev を同じ効果を持ちます。
デフォルト宣言
ある構造体が別の構造体を継承する場合、デフォルトのフィールド定義は親構造体のフィールドを子構造体のフィールドをもとにインスタンス化することができます。クリーチャーが大きいかどうかよりもより詳細なサイズが必要な場合、サイズを記述する専用のデータ型を継承と一緒に使用することができ、large フィールドを size フィールドの内容から計算するような構造体を生み出します：
inductive Size where
| small
| medium
| large
deriving BEq
structure SizedCreature extends MythicalCreature where
size : Size
large := size == Size.large
しかし、このデフォルト定義はあくまでデフォルトで与えられる定義にすぎません。C#やScalaのような言語でのプロパティ継承とは異なり、この子構造体の定義は large に特定の値が与えられない場合にのみ使用されるため、無意味な結果が生じることもあります：
def nonsenseCreature : SizedCreature where
large := false
size := .large
子構造が親構造から逸脱してはならない場合、いくつかの手段があります：
- 関係性を文書化すること、これは
BEqとHashableで行われているような感じです - それらのフィールドが適切に関係していることを示す命題を定義し、APIをその命題が真であるという根拠を重要な部分として要求するように設計すること
- 継承を全く用いない
2番目の選択肢は以下のような感じです：
abbrev SizesMatch (sc : SizedCreature) : Prop :=
sc.large = (sc.size == Size.large)
ここで等号1つは 命題の 同値を示すために使用され、等号2つは同値をチェックしてから Bool を返す関数を示すために使用されることに注意してください。SizesMatch は abbrev として定義されていますが、これは証明の際に自動的に展開され、simp で証明したい同値を示すことができるようにするためです。
ハルダー は中くらいの大きさの神話上の生き物です。もっと言うと人間と同じ大きさの生き物です。huldre の2つの大きさについてのフィールドは互いに一致します：
def huldre : SizedCreature where
size := .medium
example : SizesMatch huldre := by
simp
型クラスの継承
型クラスは、裏側では構造体だったのでした。新しい型クラスの定義は新しい構造体を定義し、インスタンスの定義はその構造体の値が作成されます。そしてこの値がLeanの内部テーブルに追加され、リクエストに応じてインスタンスを見つけることができるようになります。この結果、型クラスはほかの型クラスを継承することができます。
型クラスの継承は構造体のそれとまったく同じ言語機能を使用するため、型クラスの継承は多重継承、親の型のメソッドのデフォルト実装、菱形の自動的な折り畳みなどの構造体継承のすべての機能をサポートしています。これは、Java・C#・Kotlinのような言語で多重インターフェース継承が有用であることと多くの同じような状況で有用です。型クラスの継承階層を注意深く設計することで、プログラマは両方からいいとこ取りをすることができます：すなわち、独立に実装可能な抽象化をきめ細やかに行うこと、そしてより広く一般的な抽象化から特定の抽象化を自動的に構築することです。