LeanDB: 型安全なSQLフロントエンド

LeanDB: 型安全なSQLフロントエンド なぜか？ Lean 4では、スキーマ、クエリ、マイグレーションすべてを型にでき、コンパイラがそれらすべてをチェックします。 Harsh Gupta著 · 2026年8月27日 この記事は3つの役割を果たします。型安全なSQLフロントエンドが存在しうることを伝えること。それがなぜ価値があるのかを説明すること。最初の試作品を示し、どこが間違っているか教えてもらうこと。 以下のコード例はすべてLean 4.33でコンパイルされます。「コンパイルされない」とマークされたものは本当にコンパイルされず、コンパイラが言ったことを貼り付けています。 まず、なぜLeanなのか？ 昨年末の私の投稿「なぜエージェントコーディングにLean 4を賭けるのか？」も参照してください。 Leanや他の依存型言語を、関数型プログラミング言語の上のクラスと考えるべきです。関数型プログラミング言語では、関数を渡したり、関数を組み合わせたり、関数を別の関数の入力にしたりできます。Leanでは、型がファーストクラスオブジェクトです。抽象型を作成したり、型を組み合わせたり、型を渡したりでき、型自体が入力やパラメータを持つことができます。そしてコンパイラがそれらすべてを強制します。 3つの例。 条件付きの型 型はルールを持つことができます。ここでは年齢の型があり、そのルールは数値が150未満であることです。 def Age := { n : Nat // n < 150 } def me : Age := ⟨34, by decide⟩ このby decideは証明です。コンパイラは34 < 150をあなたのためにチェックします。 不正を試みてください: def nobody : Age := ⟨200, by decide⟩ -- コンパイルされない error: Tactic `decide` proved that the proposition 200 < 150 is false より有用なバージョンです。コンパイル時に文字列がメールアドレスかどうかはわかりません。そこで一度チェックし、型がそのチェックを記憶します。 def Email := { s : String // s.contains '@' } def Email.parse (s : String) : Option Email := if h : s.contains '@' then some ⟨s, h⟩ else none これが魔法です: hはチェックが成功したという証明です。一度Email型の値を持つと、下流の誰も@を含まない文字列を渡すことはできません。あなたも、ライブラリも、エージェントもできません。検証はちょうど一度だけ行われ、型がそのレシートを運びます。 他の型を組み合わせる型 この部分は、RustやTypeScriptを使ったことがあるなら見慣れたものに見えるでしょう。レコード、選択肢、オプションのもの。 structure Money where amount : Nat currency : String inductive Payment where | card (last4 : String) | wire (iban : String) | credit structure Order where id : Nat total : Money paidBy : Option Payment OrderはMoney、Payment、Optionから構築されています。そしてPaymentをパターンマッチするとき、コンパイラはすべてのケースを処理するようにします。 def describe : Payment → String | .card last4 => s!"card ending {last4}" | .wire iban => s!"wire from {iban}" | .credit => "store credit" .creditを忘れるとコンパイルされません。 パラメータを持つ型 これが一段上の部分です。型は値を入力を取ることができます。したがって、データベースの行はスキーマを入力を取ることができ、あるスキーマの行は別のスキーマの行とは異なる型になります。 データベースが理解する列の型から始め、それぞれをLeanの型にマッピングする関数を定義します。 inductive Ty where | int | text | bool abbrev Ty.denote : Ty → Type | .int => Int | .text => String | .bool => Bool Ty.denoteは型を返す関数です。その文はほとんどの言語では不可能です。 スキーマは名前付き列のリストです。行はそれが属するスキーマによってインデックス付けされます。 abbrev Schema := List (String × Ty) inductive Row : Schema → Type | nil : Row [] | cons {n : String} {t : Ty} {s : Schema} : t.denote → Row s → Row ((n, t) :: s) Read Row : Schema → Type を「スキーマを与えれば、型を返す」と読みます。 次にテーブルと、その中の行を定義します。 abbrev users : Schema := [("id", .int), ("email", .text), ("active", .bool)] def alice : Row users := .cons 1 (.cons "alice@example.com" (.cons true .nil)) これが全体のアイデアです。以下のすべてはそれを利用しているだけです。 なぜ型安全なデータベースが必要なのか？ 間違ったデータをプッシュしようとすると、コンパイラがそれを防いでくれます。 列の型が間違っている場合: def bob : Row users := .cons "bob" (.cons "bob@example.com" (.cons true .nil)) -- コンパイルされない error: Application type mismatch: The argument "bob" has type String but is expected to have type Ty.int.denote 列が欠落している場合: def carol : Row users := .cons 3 (.cons "carol@example.com" .nil) -- コンパイルされない error: Application type mismatch: The argument Row.nil has type Row [] but is expected to have type Row [("active", Ty.bool)] 2番目のエラーを見てください。コンパイラは、どの列を忘れたかを正確に教えてくれます。 検証を誤ってスキップした場合、コンパイラが教えてくれます。 口座からの引き出しには、口座に十分な残高がある必要があるとします。その要件を関数の型に入れます。 structure Account where id : Nat balance : Nat def withdraw (a : Account) (amt : Nat) (_ : amt ≤ a.balance) : Account := { a with balance := a.balance - amt } 3番目の引数は証明です。証明なしではwithdrawを呼び出すことはできません。 def overdraw (a : Account) : Account := withdraw a 1000000 -- コンパイルされない error: Type mismatch withdraw a 1000000 has type 1000000 ≤ a.balance → Account but is expected to have type Account 証明を得る唯一の方法は、チェックを行うことです。 def safeWithdraw (a : Account) (amt : Nat) : Option Account := if h : amt ≤ a.balance then some (withdraw a amt h) else none したがって、検証は覚えているべきことではなく、コンパイラが忘れさせてくれないことです。 これはエージェントが導入するバグのまさにそのクラスです：コードは動作し、テストはパスし、かつて存在したチェックがなくなります。ここでは、チェックがなくなることはありません。 さらに重要で興味深いのは、型付きデータベースを使用すると、他に表現するのが非常に難しいクエリを表現できることです。 コンパイル時にチェックされる列アクセス。 まず、「スキーマsに列nと型tが存在する」と言う方法が必要です。それ自体が型です。 inductive HasCol : Schema → String → Ty → Type | here {s : Schema} {n : String} {t : Ty} : HasCol ((n, t) :: s) n t | there {s : Schema} {n n' : String} {t t' : Ty} : HasCol s n t → HasCol ((n', t') :: s) n t 次に、行と列が存在するという証明を受け取るルックアップです。 def Row.get {s : Schema} {n : String} {t : Ty} : Row s → HasCol s n t → t.denote | .cons v _, .here => v | .cons _ r, .there h => r.get h def Row.col {s : Schema} (r : Row s) (n : String) {t : Ty} (h : HasCol s n t := by repeat constructor) : t.denote := r.get h このby repeat constructorは、コンパイラがコンパイル時にスキーマを検索して列を見つけるものです。列名を記述するだけです。 #eval alice.col "email" -- "alice@example.com" #eval alice.col "active" -- true 戻り値の型に注目してください。alice.col "email" はStringです。alice.col "active" はBoolです。Valueでも、Anyでも、後でキャストする文字列でもありません。結果の型は、どの列を要求したかによって異なります。 そして、タイプミス: #eval alice.col "emial" -- コンパイルされない error: unsolved goals ⊢ HasCol [] "emial" ?m.3 コンパイラはスキーマ全体を歩き回り、列がなくなったため停止しました。SQLデータベースなら深夜3時に教えてくれるでしょう。 次にJOINです。 JOINの結果スキーマは、入力スキーマから計算されます。型の中で。 def Row.append {a b : Schema} : Row a → Row b → Row (a ++ b) | .nil, r => r | .cons v l, r => .cons v (l.append r) abbrev orders : Schema := [("order_id", .int), ("total", .int)] def joined : Row (users ++ orders) := alice.append (.cons 17 (.cons 4200 .nil)) #eval joined.col "total" -- 4200 Row (users ++ orders) は、2つのリストを連結することによって計算された型です。JOINされたスキーマを自分で書き下す必要はありませんでした。コンパイラがそれを導き出し、joined.col "total" は導出されたスキーマに対して型チェックされます。ORMでこれをやってみてください。 設計目標 SQLデータベースとの前方互換性。既存のSQLデータベースをLeanDBにインポートしてすぐに使い始めることができます。あなたのCREATE TABLE users (id INTEGER, email TEXT, active BOOLEAN) はusers : Schemaになります。何も移動しません。 妥当なパフォーマンス。実際のシステムでの最終的な使用のために構築されています。型はコンパイル時にチェックされ、実行時には消去されます。証明は、実行時にはコストがかかりません。