import FormalLab.LogicAndComputation.MonadsAndComputationalEffects

/-!
# 第79章：代数的効果とハンドラ——自由な計算へ解釈を与える

モナドは効果付き計算の逐次合成を統一しますが、どの効果演算を使えるか、その演算がどの方程式を満たすかまでは
指定しません。また、計算を実行して結果を得る方法もモナド構造だけでは一意に決まりません。

本章では、**代数的効果**（algebraic effect）を演算と方程式から生成される自由な計算として捉えます。
**エフェクトハンドラ**（effect handler）は、その自由構文から別の代数への準同型として構成します。有限な選択木を
Leanで実装し、「モナド」「代数的演算」「ハンドラ」の三層が対応する条件を分離します。最後に、
表示意味論の健全性・完全性・適切性が別々の定理であることを確認します。

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

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

namespace FormalLab.LogicAndComputation.AlgebraicEffectsAndHandlers

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代数は密接に関係します。ただし実用言語のハンドラ構文は、返却節、演算節、継続の扱い、深い／
浅いハンドラなど追加の操作的選択を持ちます。一つの `T A→A` だけで全てのハンドラ仕様を表したとは限りません。

-/

/-!

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

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

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

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

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

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

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

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

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

## 要点

* 代数的効果は演算と方程式を指定し、その自由モデルが効果構文と自由モナドを与える。
* `ChoiceTree` は方程式を課す前の二択演算の自由構文であり、リストや集合とはまだ同一でない。
* ハンドラは自由な計算を対象代数へ畳み込み、採用した方程式を保存しなければならない。
* Eilenberg–Moore代数と実用言語のハンドラ構文は密接に関係するが、同じデータとは限らない。
* 操作的意味論、表示意味論、健全性、完全性、適切性は互いに異なる主張である。

## 研究史と文献案内

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

## 問題

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

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

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

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

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

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

end FormalLab.LogicAndComputation.AlgebraicEffectsAndHandlers