型クラス class と instance¶
class は，型クラスを定義するコマンドです．
型クラスは，「この型にはこの構造や操作がある」という情報を Lean に登録し，必要な場所で自動的に探すための仕組みです．
class は構文上は structure に近く，field をもつデータとして定義されます．
内部的には，通常の class ... where は structure と同様に inductive 型として扱われます．
ただし inductive が「constructor で項を作る型」を定義するコマンドであるのに対し，class はその型を型クラス探索の対象として登録し，[Add α] のような引数を Lean が自動で探せるようにする点が本質的に異なります．
instance は，特定の型に対してその field を埋めた値を登録するコマンドです．
標準ライブラリの LE，LT，Add も型クラスです．
class LE (α : Type u) where
le : α → α → Prop
class LT (α : Type u) where
lt : α → α → Prop
class Add (α : Type u) where
add : α → α → α
x ≤ y は LE.le x y の notation ですが，どの LE.le を使うかは x と y の型から決まります．
+ も同様に [Add α] から Add.add を取り出して使います．
たとえば LE.le (2 : Nat) 3 が書けるのは，Nat に対する LE Nat の instance があらかじめ登録されており，Lean がそれを型クラス探索で見つけるためです．
#check LE
#check LE.le
#check LT
#check LT.lt
#check Add
#check Add.add
example : LE.le (2 : Nat) 3 := by
decide
example : (2 : Nat) ≤ 3 := by
decide
example : Add.add (2 : Nat) 5 = 7 := by
rfl
example : (2 : Nat) + 5 = 7 := by
rfl
自分で定義した型にも，既存の数学的な型クラスの instance を登録できます．
次の Vec2 は整数成分の平面ベクトルです．
Vec2 自体は具体的なデータ型なので structure として定義し，class にする必要はありません．
class にするのは，Add のように「ある型に備わる操作や構造」を型クラス探索で扱いたい場合です．
instance : Add Vec2 を登録すると，u + v という notation が Vec2 に対して使えるようになります．
structure Vec2 where
x : Int
y : Int
deriving Repr, DecidableEq
instance : Add Vec2 where
add u v := { x := u.x + v.x, y := u.y + v.y }
def vecA : Vec2 :=
{ x := 1, y := 2 }
def vecB : Vec2 :=
{ x := 3, y := 4 }
example : vecA + vecB = { x := 4, y := 6 } := by
rfl
example : Add.add vecA vecB = { x := 4, y := 6 } := by
rfl
演習¶
型クラスを要求する関数の例として，加法を使う関数を定義してください．
また，≤ と < が型クラスの field であることを #check で確認してください．