import Mathlib.CategoryTheory.Monad.Kleisli
import Mathlib.CategoryTheory.Monad.Algebra
import FormalLab.TypedComputation.OperationalSemantics
import FormalLab.CategoricalConstructions.Monads

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

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

このように、値を返すことに失敗・状態・非決定性などの振舞いが加わることを**計算効果**
（computational effect）と呼びます。

モナド `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圏を学びました。
本章ではその構造をプログラム意味論へ接続します。例外・状態・非決定性を同じ抽象に入れても、効果の意味は
同じになりません。Kleisli射による合成、効果の層順序、値呼びの評価順序に必要な強さを区別し、モナド法則が
保証する範囲と保証しない範囲を明らかにします。

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

型 `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.LogicAndComputation.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の計算的
ラムダ計算の標準的な意味論を支えます。

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


## 要点

* `A` は値、`T A` は `A` を返す効果付き計算を表し、`pure` と `bind` が両者を接続する。
* モナド法則は自明な返却と逐次合成の括弧を消すが、効果の交換、消去、観察方法までは定めない。
* Kleisli射 `X→TY` は効果付き関数であり、Kleisli合成が `bind`、恒等射が `pure` になる。
* 例外、状態、非決定性は同じモナド接口を持ち得るが、演算、観察、方程式、効果の層順序は異なる。
* 強さ `A⊗TB→T(A⊗B)` は純粋な文脈と計算を組み合わせ、値呼び関数型の意味論を支える。

## 研究史と文献案内

Moggi [MOG91] は、値と計算を区別する計算的ラムダ計算を圏論的に定式化し、多様な計算概念をモナドで統一した
一次論文です。1989年の会議論文に先行する内容がありますが、本書の基準書誌は拡張された1991年の論文です。
モナド自体の初期史には [KLE65], [EM65]、現行Lean APIには [MATHLIB] を参照してください。

## 問題

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

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

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

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

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

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

end FormalLab.LogicAndComputation.MonadsAndComputationalEffects