提案: `Option` を `Except` に橋渡しする実践例 (`getDM` と `let some := ... | throw`)

背景

Lean by Example には Option や Monad のページがありますが、Option で返ってくる部分失敗の API を、エラーメッセージ付きの Except に自然につなぐ実践例は見当たりませんでした。

最近の Lean 公式 Zulip の lean4 ストリームで、ちょうどこのパターンをきれいに説明できる短いスレッドがありました。

• 出典: Option.toExcept or similar (lean4 stream, Feb 20 2026)
• 元の Zulip narrow link: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Option.toExcept%20or%20similar

既存掲載の確認

以下を確認し、同内容または実質同内容のページは未掲載と判断しました。

• 目次: LeanByExample/SUMMARY.lean
  • Except 専用ページは見当たりませんでした。
• 既存ページ: Type/Option.lean
  • Option 自体の説明と Functor 的な使い方はありますが、Except への橋渡しはありません。
• 既存ページ: TypeClass/Monad.lean
  • Option モナドの do 記法はありますが、失敗理由を throw に変換する話はありません。
• 既存ページ: Syntax/Match.lean
  • 一般的な match の説明はありますが、let some x := ... | throw ... という do 記法内の失敗分岐は見当たりません。
• リポジトリ検索:
  • getDM の検索
  • let some の検索
  • これらからも、今回のトピックに相当する独立した説明は見つけられませんでした。

提案したいコード例

Zulip スレッドで特に教育的だったのは、「自作 Option.toExcept を足す」よりも、Lean 既存の書き方を使うほうが自然だと示している点です。

import Std.Data.HashMap.Basic

def lookup₁ (table : Std.HashMap String (Std.HashMap String Int)) : Except String Int := do
  let x <- table["x"]?.getDM (throw "x not in table")
  let y <- x["y"]?.getDM (throw "y not in x")
  return y

import Std.Data.HashMap.Basic

def lookup₂ (table : Std.HashMap String (Std.HashMap String Int)) : Except String Int := do
  let some x := table["x"]?
    | throw "x not in table"
  let some y := x["y"]?
    | throw "y not in x"
  return y

何が面白いか

1. Option と Except の役割の違いが、短い例で一気に見える。

   • Option は「失敗した」ことしか伝えない。
   • Except は「なぜ失敗したか」まで伝えられる。

2. Lean の do 記法が、単なる逐次実行ではなく「失敗の文脈を持つ計算」の糖衣構文であることが伝わる。

   • 既存の Monad ページの続編として自然です。

3. 同じ目的に対して、Lean らしい書き方が複数ある。

   • getDM を使う書き方
   • let some x := ... | throw ... というパターン束縛の書き方

4. HashMap のネストした lookup という現実的な題材なので、抽象論で終わらない。

コードの読み方

• table["x"]? は Option (Std.HashMap String Int) を返します。
• そのままでは Except String Int の do ブロックの中で let x <- ... できません。<- の右辺は同じ失敗文脈、つまりここでは Except String _ である必要があるためです。
• そこで getDM (throw "...") を使うと、none のときに throw ... を実行し、some x のときに中身を取り出せます。
• あるいは let some x := ... | throw ... と書くと、Option をその場でパターンマッチしつつ、失敗時だけ throw できます。
• 後者は「Option を Except に変換している」というより、「do 記法の中で失敗分岐を明示している」読み方ができるのが面白いです。

Lean by Example に追加する価値

• 既存の Option / Monad / match のページを横断する、実践的なブリッジ例になっています。
• 初学者がかなり早い段階で遭遇する「Option の API を Except ベースの関数の中でどう扱うか」という疑問に直接答えます。
• Zulip の元投稿でも、質問者は自作 Option.toExcept を考えていましたが、返信では Lean 既存のイディオムが提示されていました。この「自作したくなるが、実は標準的な書き方がある」という流れ自体が教材として強いです。
• 1ページに収まる小ささでありながら、do 記法・失敗・パターン束縛・エラーハンドリングを同時に説明できます。

曖昧な点と前提

• 「未掲載」の判定は、Option や Monad を一般に説明するページが既にあることを踏まえつつも、Option から Except への橋渡しを主題にした実質同内容の例はまだない、という前提で行っています。
• lookup₁ / lookup₂ という名前は説明用の仮名です。Lean by Example に載せるなら、ページ全体の文脈に合わせてより説明的な名前に変えてよいと思います。
• getDM と let some := ... | ... のどちらを主役にするかは編集方針次第ですが、個人的には両方並べると比較が効いてよいと思います。

Start by reading LeanByExample/SUMMARY.lean, Type/Option.lean, TypeClass/Monad.lean, and Syntax/Match.lean to follow the existing page structure and avoid duplication. Add a focused example page covering both the getDM and let some patterns shown in the issue, then link it from the summary and verify the examples fit the existing documentation conventions.