import Mathlib.CategoryTheory.Monad.Kleisli
import Mathlib.CategoryTheory.Monad.Algebra
import FormalLab.TypeTheory.OperationalSemantics
import FormalLab.CategoryTheory.Monads

/-!
# 第77章：モナドと計算効果——値から計算を分離して合成する

純粋な関数 `f:A→B` は、入力値から出力値を返します。失敗し得る関数は `A→Option B`、状態を読み書きする関数は
`A→S→B×S`、複数の結果を返す関数は `A→List B` という異なる型になります。これらを通常の関数合成でつなぐと、
中間に現れる失敗、状態、分岐を毎回手作業で処理しなければなりません。

モナド `T` は「`B` の値を返す効果付き計算」を `T B` と表し、純粋な値を計算へ入れる操作と、計算の結果を使って
次の計算を選ぶ操作を統一します。

$$
\mathsf{pure}:A\longrightarrow T A,
\qquad
\mathsf{bind}:T A\longrightarrow(A\to T B)\longrightarrow T B.
$$

第53章では、これを自己関手、単位 `η`、乗法 `μ` として定義し、Kleisli圏とEilenberg–Moore圏を学びました。
本章ではその構造をプログラム意味論へ接続します。例外・状態・非決定性を同じ抽象に入れても、効果の意味は
同じになりません。評価順序には強さが関わります。さらに、代数的演算とハンドラが自由代数の普遍性をどう
利用するかを明らかにします。

## 値と計算は異なる型を持つ

型 `A` は既に得られた値、`T A` は実行すると `A` を返す計算を表します。`pure` は効果を起こさず値を返します。
`bind m k` は計算 `m:T A` を実行し、成功して得た `a:A` に応じて次の計算 `k a:T B` を選びます。

三つの法則は、意味を変えない余分な `pure` を除き、三段以上の逐次計算の括弧を一意にします。

$$
\begin{aligned}
\mathsf{bind}(\mathsf{pure}(a),k)&=k(a),\\
\mathsf{bind}(m,\mathsf{pure})&=m,\\
\mathsf{bind}(\mathsf{bind}(m,k),h)
  &=\mathsf{bind}(m,a\mapsto\mathsf{bind}(k(a),h)).
\end{aligned}
$$

これらは効果を消す法則ではありません。同じ効果を起こす計算を、逐次合成の括弧や自明な返却に依存せず記述する
ための法則です。

## 例外では失敗した時点で残りを飛ばす

例外型 `Except ε A` は、例外 `ε` または正常値 `A` を持ちます。`bind` は例外ならそのまま返し、正常値だけを
継続へ渡します。
-/

namespace FormalLab.Bridges.MonadsAndComputationalEffects

def exceptPure {ε α : Type} (value : α) : Except ε α := .ok value

def exceptBind {ε α β : Type} (computation : Except ε α)
    (next : α → Except ε β) : Except ε β :=
  match computation with
  | .error error => .error error
  | .ok value => next value

theorem except_left_unit {ε α β : Type} (value : α) (next : α → Except ε β) :
    exceptBind (exceptPure value) next = next value := rfl

theorem except_right_unit {ε α : Type} (computation : Except ε α) :
    exceptBind computation exceptPure = computation := by
  cases computation <;> rfl

theorem except_assoc {ε α β γ : Type} (computation : Except ε α)
    (first : α → Except ε β) (second : β → Except ε γ) :
    exceptBind (exceptBind computation first) second =
      exceptBind computation (fun value => exceptBind (first value) second) := by
  cases computation <;> rfl

def safePredecessor : Nat → Except String Nat
  | 0 => .error "zero has no predecessor"
  | n + 1 => .ok n

def twoPredecessors (number : Nat) : Except String Nat :=
  exceptBind (safePredecessor number) safePredecessor

example : twoPredecessors 3 = .ok 1 := rfl
example : twoPredecessors 1 = .error "zero has no predecessor" := rfl

/-!
二つ目の計算では、最初の前者計算は成功して `0` を返し、二回目が例外になります。その後に継続があっても
`exceptBind` は実行しません。三法則は例外の発生位置を移動しません。括弧を変えても、左から同じ順に計算して
最初の例外を返すことを保証します。

## 状態では結果と次の状態を同時に返す

状態型を `σ` とすると、`State σ α = σ→α×σ` です。計算は初期状態を受け取り、値と更新後の状態を返します。
逐次合成は最初の計算が返した状態を二番目へ渡します。
-/

abbrev StateComputation (σ α : Type) := σ → α × σ

def statePure {σ α : Type} (value : α) : StateComputation σ α :=
  fun state => (value, state)

def stateBind {σ α β : Type} (computation : StateComputation σ α)
    (next : α → StateComputation σ β) : StateComputation σ β :=
  fun initial =>
    let result := computation initial
    next result.1 result.2

theorem state_left_unit {σ α β : Type} (value : α)
    (next : α → StateComputation σ β) :
    stateBind (statePure value) next = next value := rfl

theorem state_right_unit {σ α : Type} (computation : StateComputation σ α) :
    stateBind computation statePure = computation := by
  funext initial
  change ((computation initial).1, (computation initial).2) = computation initial
  exact Prod.eta _

theorem state_assoc {σ α β γ : Type} (computation : StateComputation σ α)
    (first : α → StateComputation σ β) (second : β → StateComputation σ γ) :
    stateBind (stateBind computation first) second =
      stateBind computation (fun value => stateBind (first value) second) := by
  funext initial
  cases computation initial
  rfl

def getState {σ : Type} : StateComputation σ σ :=
  fun state => (state, state)

def putState {σ : Type} (newState : σ) : StateComputation σ Unit :=
  fun _ => ((), newState)

def tick : StateComputation Nat Nat :=
  fun state => (state, state + 1)

def tickTwice : StateComputation Nat (Nat × Nat) :=
  stateBind tick fun first =>
    stateBind tick fun second =>
      statePure (first, second)

example : tickTwice 5 = ((5, 6), 7) := rfl

/-!
`tickTwice` は最初に `5` を観察して状態を `6` にし、次に `6` を観察して `7` にします。状態の受け渡し順を
反転すれば一般に別の結果になります。モナド結合律は計算順序を交換する可換律ではなく、同じ左から右の列に
付けた括弧だけを変えます。

## 同じインターフェースでも効果は区別される

例外と状態はどちらも `pure` と `bind` を持ち、同じ三法則を満たします。しかし `Except ε α` と
`State σ α` の要素、観察、等価性は異なります。モナドは効果の逐次合成に共通する形を抽出しますが、どの演算が
利用できるか、計算をどう実行するか、二計算をいつ等しいとみなすかを一つには決めません。

非決定性なら `T A` を有限な候補のリストや有限集合で表せます。リストを用いる場合、`bind` は各候補へ継続を
適用して結果を連結します。リストは順序と重複を保持するため、集合的な非決定性とは法則が異なります。確率、
入出力、継続、並行性も、それぞれ追加構造と観察同値を確認する必要があります。

効果の組合せにも順序があります。`State σ (Except ε A)` は例外とともに状態更新を失う表現になり得ますが、
`Except ε (State σ A)` は型の意味から別物です。実際のモナド変換子では、どちらの層を外側に置くかがrollbackや
例外時の状態保持へ影響します。「モナド同士は常に自動的に合成できる」とは限りません。合成には分配法則などの
追加条件を要します。

## Kleisli射は効果付き関数である

圏 `C` 上のモナド `T` について、Kleisli射 `X⇝Y` は元の圏の射 `X→T Y` です。二射

$$
f:X\longrightarrow T Y,
\qquad g:Y\longrightarrow T Z.
$$

の合成は `X→TY→T²Z→TZ` と進みます。`T.map g` は効果の内側の値へ次の計算を差し込み、`μ` が二重の計算を
一段へ平坦化します。
-/

open _root_.CategoryTheory

universe uC vC

variable {C : Type uC} [Category.{vC} C]
variable (T : Monad C)
variable {X Y Z W : C}

def asKleisli (f : X ⟶ T.obj Y) :
    Kleisli.mk T X ⟶ Kleisli.mk T Y :=
  ⟨f⟩

def kleisliComposite (f : X ⟶ T.obj Y) (g : Y ⟶ T.obj Z) : X ⟶ T.obj Z :=
  f ≫ T.map g ≫ T.μ.app Z

theorem kleisli_composite_is_category_composition
    (f : X ⟶ T.obj Y) (g : Y ⟶ T.obj Z) :
    (asKleisli T f ≫ asKleisli T g).of = kleisliComposite T f g := rfl

theorem kleisli_associative (f : X ⟶ T.obj Y) (g : Y ⟶ T.obj Z)
    (h : Z ⟶ T.obj W) :
    (asKleisli T f ≫ asKleisli T g) ≫ asKleisli T h =
      asKleisli T f ≫ (asKleisli T g ≫ asKleisli T h) :=
  Category.assoc _ _ _

/-!
最後の定理はKleisli圏の結合律です。mathlibの圏インスタンス内部では、この証明を `T.map` の関手性、`μ` の
自然性、モナド結合律へ還元しています。単に一般の圏法則を引用したように見えても、Kleisli圏を圏として構成する
段階で必要な計算は既に検査されています。

Kleisli圏の恒等射は `η_X:X→TX` です。従って純粋な値返却が効果付き関数の恒等になり、Kleisli合成が `bind` に
なります。プログラミング言語で用いる `pure` と `bind` は、圏論的な `η` と `μ` を別の基本演算へ組み替えた
表示です。

## 値呼びの項はKleisli射として読める

純粋STLCでは判断 `Γ⊢t:A` を関数 `⟦Γ⟧→⟦A⟧` と解釈しました。値呼びの効果付き計算では

$$
\llbracket\Gamma\vdash t:A\rrbracket:
\llbracket\Gamma\rrbracket\longrightarrow T\llbracket A\rrbracket.
$$

と解釈します。代入で先の計算結果を次の項へ渡すと、通常の関数合成ではなくKleisli合成になります。`return` は
`η`、`let x←m; n` は `bind` です。

関数値の型 `A→B` は、値 `A` を受け取って `B` の計算を返す内部関数 `A⇒TB` として解釈できます。適用時に
関数部分と引数部分も効果を持つなら、どちらを先に評価するかを指定しなければなりません。第13章の値呼びが
関数から引数へ進む順序は、表示意味論ではモナドと積の相互作用へ移ります。

## 強さは純粋な文脈と効果付き計算を組み合わせる

モノイダル圏上の強いモナドは、自然な射

$$
\mathsf{st}_{A,B}:A\otimes T B\longrightarrow T(A\otimes B).
$$

を持ちます。これは純粋な値 `A` を保持したまま `B` の計算を実行し、対を計算の内側へ入れます。`Type` と
状態モナドでは次の関数です。
-/

def stateStrength {σ α β : Type} :
    α × StateComputation σ β → StateComputation σ (α × β) :=
  fun pair initial =>
    let result := pair.2 initial
    ((pair.1, result.1), result.2)

example : stateStrength (σ := Nat) ("count", tick) 4 = (("count", 4), 5) := rfl

/-!
一般のモノイダル圏では、モナド構造だけからstrengthが自動的に得られるとは限りません。strengthには自然性、
単位子・結合子との整合性、`η`・`μ` との両立が必要です。デカルト閉圏上の強いモナドが、Moggiの計算的
ラムダ計算の標準的な意味論を支えます。

左から右と右から左の二つの評価を比較して常に一致するなら、モナドの可換性に相当する条件が現れます。状態、
例外の優先順位、入出力などは一般に順序を観察できるため、任意のモナドを可換と仮定してはいけません。結合律は
括弧を消しますが、交換律は与えません。

## 代数的効果は演算と方程式から自由に計算を作る

モナドを先に与える代わりに、効果演算のシグネチャと方程式を与え、その自由モデルからモナドを構成できます。
例として、値を返す葉と二択演算だけを持つ有限な選択木を作ります。
-/

inductive ChoiceTree (α : Type) where
  | pure : α → ChoiceTree α
  | choose : ChoiceTree α → ChoiceTree α → ChoiceTree α
  deriving DecidableEq, Repr

def ChoiceTree.bind {α β : Type} : ChoiceTree α → (α → ChoiceTree β) → ChoiceTree β
  | .pure value, next => next value
  | .choose left right, next => .choose (bind left next) (bind right next)

theorem ChoiceTree.left_unit {α β : Type} (value : α) (next : α → ChoiceTree β) :
    ChoiceTree.bind (.pure value) next = next value := rfl

theorem ChoiceTree.right_unit {α : Type} (tree : ChoiceTree α) :
    ChoiceTree.bind tree .pure = tree := by
  induction tree with
  | pure => rfl
  | choose left right leftIH rightIH => simp [ChoiceTree.bind, leftIH, rightIH]

theorem ChoiceTree.assoc {α β γ : Type} (tree : ChoiceTree α)
    (first : α → ChoiceTree β) (second : β → ChoiceTree γ) :
    ChoiceTree.bind (ChoiceTree.bind tree first) second =
      ChoiceTree.bind tree (fun value => ChoiceTree.bind (first value) second) := by
  induction tree with
  | pure => rfl
  | choose left right leftIH rightIH => simp [ChoiceTree.bind, leftIH, rightIH]

/-!
`ChoiceTree` は方程式をまだ課していない二項演算の自由構文です。選択の交換律、結合律、冪等律を商で課せば、
順序や重複を観察しない別の非決定性になります。自由構文をリストや集合と最初から同一視すると、どの方程式を
採用したかが見えなくなります。

## ハンドラは自由な計算を別の代数へ畳み込む

選択木のハンドラは、純粋な値の解釈 `returnCase:α→β` と、二択結果を結ぶ演算 `chooseCase:β→β→β` を指定します。
自由性により、木全体の解釈は構造再帰で一意に決まります。
-/

def handleChoice {α β : Type} (returnCase : α → β) (chooseCase : β → β → β) :
    ChoiceTree α → β
  | .pure value => returnCase value
  | .choose left right =>
      chooseCase (handleChoice returnCase chooseCase left)
        (handleChoice returnCase chooseCase right)

def allOutcomes {α : Type} : ChoiceTree α → List α :=
  handleChoice (fun value => [value]) List.append

def firstOutcome? {α : Type} : ChoiceTree α → Option α :=
  handleChoice some fun left right => left.orElse fun _ => right

def sampleChoice : ChoiceTree Nat :=
  .choose (.pure 1) (.choose (.pure 2) (.pure 3))

example : allOutcomes sampleChoice = [1, 2, 3] := rfl
example : firstOutcome? sampleChoice = some 1 := rfl

/-!
同じ計算木を、全候補の列または最初の候補として解釈できました。ハンドラは効果を「消す」魔法ではなく、演算を
別の代数で解釈します。正しいハンドラは、効果理論に課した方程式を保存しなければなりません。自由代数からの
準同型の一意性が、構造再帰と合成可能性の数学的根拠になります。

Eilenberg–Moore代数 `a:T A→A` は、モナドが表す自由計算を `A` へ整合的に解釈します。従って代数的ハンドラと
Eilenberg–Moore代数は密接に関係します。ただし実用言語のhandler構文は、返却節、演算節、継続の扱い、深い／
浅いハンドラなど追加の操作的選択を持ちます。一つの `T A→A` だけで全てのhandler仕様を表したとは限りません。

## 全ての効果が同じ意味で代数的とは限らない

例外、非決定性、入出力、状態は、適切な演算と方程式による代数的効果として扱えます。一方、継続や局所状態の
スコープなどは、素朴な一階代数演算の枠をそのまま適用できない場合があります。高階効果、scoped effect、
effect handlerの諸体系は、この境界を異なる方法で拡張します。

従って「効果はモナドである」「効果は代数的演算である」「効果はハンドラで処理する」という三文は同値な定義では
ありません。モナドは逐次合成、代数理論は演算と方程式、ハンドラは解釈の変更を中心にします。対象とする効果と
言語に応じて、三層の対応条件を示す必要があります。

## 表示意味論と操作的意味論は別の役割を持つ

第13章の小ステップ意味論は、項が次にどの状態へ進むかを定めます。本章のモナド意味論は、項を数学的な射へ移し、
プログラム等価性を射の等式として研究します。表示が等しい二項の小ステップ列が同一である必要はありません。
逆に同じ値へ停止するだけでは、状態変更、例外、入出力などの観察が等しいとは限りません。

意味論の健全性は、構文上の等式や簡約が表示の等式を保つことです。十分なモデル族に対する完全性は、表示が等しい
項の等式を構文で導けることです。adequacyは、停止や観察結果のような操作的性質と表示を結びます。これらを
「モナド則が成り立つ」ことだけから一括して結論はできません。

## 現行mathlibが形式化する境界

mathlibの `Monad C` は自己関手、`η`、`μ` と三法則を持ちます。`Kleisli T` と `T.Algebra` はKleisli圏と
Eilenberg–Moore圏を構成します。本章の `kleisli_associative` は、構成済みのKleisli圏の結合律を再利用します。

`exceptBind`, `stateBind`, `ChoiceTree` は、意味を要素ごとに観察するため本章で定義した小さなモデルです。Leanの
プログラミング用 `Monad` 型クラスと圏論の `CategoryTheory.Monad` は対応しますが、同じstructureではありません。
強いモナド、モナド変換子、代数的効果シグネチャ、handler言語の全てを現行の単一APIが自動的に結ぶわけでも
ありません。

## 要点

* `A` は値、`T A` は `A` を返す効果付き計算を表し、`pure` と `bind` が両者を接続する。
* モナド法則は自明な返却と逐次合成の括弧を消すが、効果の交換や消去を述べない。
* Kleisli射 `X→TY` は効果付き関数であり、Kleisli合成が `bind`、恒等射が `pure` になる。
* 例外、状態、非決定性は同じモナド接口を持ち得るが、演算、観察、方程式は異なる。
* 強さ `A⊗TB→T(A⊗B)` は純粋な文脈と計算を組み合わせ、値呼び関数型の意味論を支える。
* 代数的効果は演算と方程式から自由モナドを作り、ハンドラは自由代数から別の代数への準同型として読める。
* 操作的意味論、表示意味論、健全性、完全性、adequacyは互いに異なる主張である。

## 研究史と文献案内

Moggi [MOG91] は、値と計算を区別する計算的ラムダ計算を圏論的に定式化し、多様な計算概念をモナドで統一した
一次論文です。1989年の会議論文に先行する内容がありますが、本書の基準書誌は拡張された1991年の論文です。
Haskellなど後代の言語におけるAPIを、同論文の構文や目的へそのまま遡及させません。

PlotkinとPower [PP03] は代数的演算とgeneric effectの対応を研究した一次論文です。PlotkinとPretnar [PP13] は
自由モデルと準同型を基盤として、例外処理を一般の代数的効果ハンドラへ拡張しました。2009年の会議版と2013年の
査読誌版は題名と内容が完全には同一でないため、本書では後者を引用します。モナド自体の初期史には [KLE65],
[EM65]、現行Lean APIには [MATHLIB] を参照してください。

## 問題

### 三つの具体モナドを同じ法則で比較する

`Except ε`, `State σ`, `List` について `pure` と `bind` を定義し、左右単位律と結合律を証明してください。
証明で用いる場合分けまたは帰納法を並べ、各モナドで法則の同じ箇所がどの具体計算になるかを比較します。次に
例外の優先順位、状態の最終値、リストの順序と重複という観察を一つずつ選び、三法則だけでは同一視されないことを
反例で示せば完了です。

### 値呼び適用の表示をstrengthから構成する

`f:Γ→T(A⇒TB)` と `a:Γ→TA` を持つ値呼び適用を考えます。対角射で文脈を二つへ分け、strengthを使って関数計算と
引数計算を左から右へ逐次化し、評価射を `T` の内側で適用する合成を書いてください。逆順の合成も書き、可換でない
状態モナドでは両者が異なる例を計算します。結合子、対角射、strength、`μ` の各使用箇所を型検査できれば完了です。

### ChoiceTreeの自由性を証明する

型 `β`、写像 `r:α→β`、二項演算 `c:β→β→β` を固定します。`handleChoice r c` が葉と選択を保存する準同型で
あることを示し、同じ二条件を満たす任意の関数 `h:ChoiceTree α→β` が `handleChoice r c` と等しいことを木の
帰納法で証明してください。次に選択の結合律・交換律・冪等律を商で課す場合、対象代数 `c` に必要な法則を一つずつ
対応させれば完了です。

### 例外ハンドラをEilenberg–Moore代数として調べる

例外ごとの既定値 `recover:ε→A` から関数 `Except ε A→A` を作ります。これが例外モナドの単位と乗法を保存する
Eilenberg–Moore代数であることを場合分けで証明してください。次に例外を別の例外型へ再送出するhandlerを考え、
終域が `A` ではなく別の自由代数になることを説明します。handler構文と固定対象上の代数を同一視できない境界を
具体的な型で示せば完了です。

### 効果の層順序を状態と例外で比較する

状態更新の後に例外を投げる計算を、`σ→Except ε (A×σ)` と `σ→Except ε A×σ` に相当する二つの表現で構成します。
例外時に更新をrollbackする意味と保持する意味を、初期状態を与えて計算してください。両表現の間に自然な変換を
作る際に失われる情報を特定し、モナド合成に必要な分配法則が単なる型の入れ替えではない理由を説明できれば
完了です。

### 表示の健全性とadequacyを分ける

例外付き値呼びラムダ計算の小さな構文と一段簡約を定義し、`raise` がbindの残りを飛ばす規則を加えてください。
各一段簡約が `Except` モナド表示の等式を保つことを構文帰納法で示します。その後、閉じた項の表示が `.ok v` なら
項が値 `v` へ到達する、という適切性の候補を述べてください。この方向は健全性だけでは証明できません。必要な
論理関係または計算可能性議論を特定できれば完了です。
-/

end FormalLab.Bridges.MonadsAndComputationalEffects