BOOK-2 — 関数型プログラミング入門 in Lean 4
¥3,999($26.28)
International shipping available
BOOK-2
関数型プログラミング入門 in Lean 4
型を通すことではなく、性質を証明しながら発見していく、AI時代の関数型プログラミング
A Discovery-Driven Tutorial on Functional Programming in Lean 4
Ken Okabe
目次
Unit 0: 招待
§1 パイプライン哲学
データ変換パイプライン
パイプラインのスケーリング：関数合成の技術
その他の基本的なプログラミング概念
関数型パイプラインの統一的な可能性
§2 なぜ「型が通る」だけでなく「発見しながら作る」のか
発見駆動という学び方——定義を教わるのではなく、壊れる場面から立ち上げる
二重の読者像：AIが書く／人間も書ける
前方参照を作らない、という設計方針
画像の再利用方針
§3 目次
Unit 1: 関数による構築
§1 制御フロー
構造化プログラミングの基礎：順次・選択・反復
再帰：関数型反復の基礎
§2 式
パイプラインと式（Leanの|>）
第一級関数
高階関数
§3 型とラムダ
型：スムーズなパイプラインの保証
ラムダ式（fun記法）
依存関数型 (x : α) → β x — 通常の関数型言語にはない、Lean固有の強み
ジェネリック関数型：α → βの力とHOFの型分解
§4 二項演算
二項演算とパイプライン演算子
カリー化と部分適用
flipとパイプラインの再構成
§5 依存グラフ
コードをどう動かすか：依存グラフによるコード駆動
ループする依存グラフと再帰の関係
純粋関数型言語という、Leanの立ち位置（IOへの予告）
§6 用語と概念
関数型プログラミングの用語を、Leanのキーワードに対応づけて整理する
Unit 2: 代数的構造
§1 代数的構造とパイプラインフロー
§2 モノイド
結合律：堅牢な構造の構築
半群：最初の代数的構造（ゼロから自作）
単位元：演算における中立な値
モノイド：単位元を持つ半群
Lean証明：結合律・単位元則をtheoremとして実際に証明する（term-mode）
§3 合成則
関数合成という自然なモノイド
§4 集合論と圏論
集合論と型：深く見る
圏論の最小限の導入
§5 ファンクタ
ファンクタ：関数間のマッピング（ゼロから自作）
§6 モナド
世界をつなぐもう一つの橋
クライスリの矢
モナド：ゼロから自作
§7 ファンクタ／モナド則
ファンクタ則をLeanのtheoremとして証明する（term-mode）
モナド則（結合律・単位元則）をtactic-modeで証明する
Unit 3: 一般的なファンクタとモナド
§1 恒等ファンクタ／モナド
§2 Listファンクタ／モナド
§3 Optionファンクタ／モナド
§4 Result(Except)ファンクタ／モナド
§5 IOファンクタ／モナド
Unit 4: 並列計算（Applicative）
§1 Two Bridges再訪とapply/map2の発見
mapをmyIDとmyApplyへ分解する
HOFの持ち上げとしてのapply
§2 二項演算としてのmap2
map2は二項演算をコンテナへ持ち上げる代数構造である
§3 デカルト積とポイントワイズ（Zip）
Listに対する2つの独立した合法な実装パターンの解剖
§4 実世界における並列処理パターン
デカルト積とZip、それぞれが適する場面の実務的な使い分け
§5 分類木とアプリカティブファンクターの定義
Functor・Monadと並ぶ体系としての、Applicative Functorの位置づけ
§6 アプリカティブ則
Applicativeの4法則をLeanのtheoremとして実際に証明する
§7 アプリカティブ則の実務的な意味
4法則が「独立性」という直感の後付けの形式化であることを見る
§8 Haskellの「理論的優位性」という神話——圏論的視点からの批判的検証
Functor ⊆ Applicative ⊆ Monadという型クラス階層は圏論的必然ではなく、Haskellのエンジニアリング上の設計選択であることの検証
Listに対するデカルト積とZipという、圏論的に等しく正当な複数のApplicative構造の共存
coherenceという語の圏論的意味とPL理論的意味の違い、Lean/mathlibのdiamond問題との比較
自動解決というトレードオフの評価と、Leanが採る折衷的設計
§9 特別編：次世代のAIが学習するかもしれない話
AIの学習データが特定コミュニティの解釈に偏ることについての批判的考察
Unit 5: Timeline FRP（概念編）
§1 不変の世界とFRP
不変の世界（ブロックユニバースモデル）という思想
FRPはスプレッドシートに似ている
§2 コアAPIの型シグネチャと法則
map：静的な依存関係の型
bind：動的な依存関係の型
using：外部リソースとのライフサイクル同期の型
Functor/Monad則の再検証（型シグネチャと法則のみ。フルライブラリ実装はスコープ外）
Unit 6: エピローグ
§1 発見駆動学習が残すもの
§2 特別編：AI時代のLean 4コーディング体験
