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

[Seasawher]

たしかに、普通の 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 由来のマジックとしても筋がいい。