型クラスマジック: Prolog みたいな探索をやる

たしかに、普通の Pretty とか OfNat は弱い。
Lean で「型クラスマジック」と呼べるのは、次の方向。

1. 型クラスで可変長引数関数を作る

Haskell の printf 系マジック。
型クラスのインスタンスを

result
α → result
β → α → result
...

みたいに再帰的に合成して、任意個の引数を取れるようにする。

class VariadicSum (α : Type) where
go : Nat → α
instance : VariadicSum Nat where
go acc := acc
instance [VariadicSum α] : VariadicSum (Nat → α) where
go acc := fun n => VariadicSum.go (acc + n)
def sumAll [VariadicSum α] : α :=
VariadicSum.go 0
#eval (sumAll : Nat)
-- 0
#eval (sumAll 10 20 30 : Nat)
-- 60

これはけっこう本物のマジック。
sumAll 自体は引数を取らないのに、期待される型が Nat → Nat → Nat → Nat なら、その型に合うインスタンスが再帰的に生成される。

Haskell の variadic function は「最終結果型」と「さらに引数を取る関数型」のインスタンスを分けるパターンで実装できる、と説明されている。C の printf みたいな非型安全 variadic と違って、この方式は型クラス解決で型安全にやる。

⸻

2. 型レベル printf

さらに真面目にやるなら、フォーマット列を型に持ち上げる。

雰囲気はこう。

inductive Fmt where
| done
| lit : String → Fmt → Fmt
| nat : Fmt → Fmt
| str : Fmt → Fmt
def Fmt.denote : Fmt → Type
| .done => String
| .lit _ k => k.denote
| .nat k => Nat → k.denote
| .str k => String → k.denote
class Printf (f : Fmt) where
printfAux : String → f.denote
instance : Printf .done where
printfAux acc := acc
instance [Printf k] : Printf (.lit s k) where
printfAux acc := Printf.printfAux (acc ++ s)
instance [Printf k] : Printf (.nat k) where
printfAux acc := fun n =>
Printf.printfAux (acc ++ toString n)
instance [Printf k] : Printf (.str k) where
printfAux acc := fun s =>
Printf.printfAux (acc ++ s)
def printf (f : Fmt) [Printf f] : f.denote :=
Printf.printfAux ""
#eval printf (.lit "x = " (.nat (.lit ", name = " (.str .done)))) 10 "Lean"
-- "x = 10, name = Lean"

ここで起きていること：

printf fmt

の返り値の型が、fmt の構造から

Nat → String → String

に変わる。

これはかなり「型クラスマジック」。
普通の関数では、値 fmt に応じて返り値の型を変えるのは難しい。依存型 + 型クラスでやる。

⸻

3. HList から「型で」値を取り出す

Haskell の heterogeneous list / extensible record 系。

inductive HList : List Type → Type where
| nil : HList []
| cons : α → HList xs → HList (α :: xs)
class HasType (α : Type) (xs : List Type) where
get : HList xs → α
instance : HasType α (α :: xs) where
get
| .cons x _ => x
instance [HasType α xs] : HasType α (β :: xs) where
get
| .cons _ xs => HasType.get xs
def hget {α xs} [HasType α xs] (xs' : HList xs) : α :=
HasType.get xs'
def row : HList [Nat, String, Bool] :=
.cons 42 (.cons "hello" (.cons true .nil))
#eval hget row Nat
#eval hget row String
#eval hget row Bool

ただしこれは重複型があると危険。

HList [Nat, Nat]

で Nat を取ると、先頭の Nat が選ばれる。
なので実用上は「ラベル付きフィールド」にする。

⸻

4. ラベル付き extensible record

型クラス探索で「このレコードは name : String フィールドを持つ」を証明させる。

structure Field where
name : String
type : Type
inductive Row : List Field → Type where
| nil : Row []
| cons : (label : String) → α → Row xs →
Row ({ name := label, type := α } :: xs)
class HasField (label : String) (α : Type) (xs : List Field) where
get : Row xs → α

あとは

HasField "name" String xs
HasField "age" Nat xs

を型クラス探索で解かせる。

これは Haskell の HasField / extensible records に近い。
Lean でも GetElem, Coe, OfNat, HAdd みたいな標準機構は、かなりこの思想で動いている。Lean 公式マニュアルでも、インスタンス探索は型クラスの中核機構として説明され、outParam / semiOutParam によって「入力型から出力型を決める」探索を制御できる。

⸻

5. 型クラスで「型レベル関数」を実装する

これは一番 Lean らしい。

class AssocType (α : Type) where
Output : Type
default : Output
instance : AssocType Nat where
Output := String
default := "nat"
instance : AssocType Bool where
Output := Nat
default := 0
def getDefault (α : Type) [AssocType α] : AssocType.Output α :=
AssocType.default
#eval getDefault Nat
#eval getDefault Bool

Nat ↦ String, Bool ↦ Nat みたいな対応を型クラスで持つ。
Haskell なら associated type family。

Lean では outParam を使うと、もっと functional dependency っぽくできる。

class KeyVal (key : Type) (val : outParam Type) where
value : val
instance : KeyVal Nat String where
value := "Nat maps to String"
instance : KeyVal Bool Nat where
value := 123
#eval (KeyVal.value : String)
#eval (KeyVal.value : Nat)

outParam は「そのパラメータを探索の入力ではなく出力として扱う」ための機構。Lean の Functional Programming in Lean でも、outParam は型クラス探索の制御に使うものとして説明されている。

⸻

6. 型クラスで Prolog 的探索をする

たとえば型レベル自然数。

inductive TNat where
| z
| s : TNat → TNat
class AddT (a b c : TNat) where
instance : AddT .z b b where
instance [AddT a b c] : AddT (.s a) b (.s c) where

これで

AddT 2 3 ?x

みたいな関係を型クラス探索で解く。
Lean の型クラスは本質的に Horn clause 的に使える。

面白いのは、これは「関数」ではなく「関係」なので、書き方次第で論理プログラミングになること。

class Member (α : Type) (xs : List Type) where
instance : Member α (α :: xs) where
instance [Member α xs] : Member α (β :: xs) where

これは「α が型リスト xs に含まれる」を探索で証明している。

⸻

7. Mathlib の algebra hierarchy は巨大な型クラスマジック

これは実用面で本命。

[Group G]
[TopologicalSpace G]
[IsTopologicalGroup G]

みたいな構造を積み上げると、定理に必要な補助構造が自動で供給される。

Anne Baanen の “Use and abuse of instance parameters in the Lean mathematical library” は、mathlib が型クラスを大規模に使って数学的構造を組織していること、その設計上の問題と対処を分析している。

これは「面白い小技」ではなく、Lean における本物の型クラス利用例。

⸻

8. 一番ネタとして強い候補

本に載せるなら、順番はこれがいい。

1. 可変長 sumAll
   • すぐ驚ける。
   • コードが短い。
2. 型付き printf
   • Haskell 由来っぽさが強い。
   • 「フォーマットから関数型が生成される」が面白い。
3. HList / extensible record
   • 型クラス探索がデータ構造探索になる。
   • Lean の依存型と相性がいい。
4. 型レベル Prolog
   • 型クラスはただの overloading ではなく、探索エンジンだと分かる。

前回より真面目に選ぶなら、Lean で一番「おっ」となるのは 型付き printf か HList フィールド検索。
Haskell 由来のマジックとしても筋がいい。

No file, chapter, or test is named. Start by inspecting the repository's existing example and book structure, then compare this proposal's suggested ordering and topics with the current contents. Done means agreeing on a focused scope and adding the selected type-class examples in the project's established format.