TL;DR
- 提唱者の見方では、代数的エフェクトは operation とそれが満たす等式（等式理論）で表せる計算エフェクトであり、その自由モデルからモナドが導かれる。
- ハンドラーは等式理論のモデルに当たり、ハンドリングは自由モデルからそのモデルへの準同型として説明できる。
- 実用言語では等式を言語機能として直接書かないことが多いので、ハンドラーが法則を満たすかは仕様やテストで確かめる。
内容
ざっくりした説明
発表者は代数的エフェクトを「operation によって計算エフェクトを表現したもの」とまず定義する。operation（get、set など）自体は具体的な処理を行わず、処理を与えるのがハンドラーである。同じ operation の組み合わせでもハンドラーを差し替えれば、本番とテストで別の処理ができる。Koka で State エフェクトの宣言、それを使う関数、ハンドラーを示したうえで、「このコードのどこに代数があるのか」と問いを立てる。
提唱者による定義
Plotkin と Pretnar の論文（2013）の説明では、代数的エフェクトとはエフェクトを生む operation を持つ等式理論で表せる計算エフェクトであり、その理論の自由モデルが計算モナドを誘導する。Moggi は計算エフェクトをモナドでモデル化したが、Plotkin と Power（2002）は、計算エフェクトはモナドを決定するがモナドと同一視はしないという立場を取った。どちらもモナドに行き着くが、代数的エフェクトの見方では、モナドは operation と等式から結果として現れる。
等式理論と Σ-木
operation の並びは木（Σ-木）として描ける。get は得られた状態値ごとに枝分かれし、set は値を記録して一本道で進む。State には「set を二回続けると最後の set だけが残る」「set の直後に get すると set した値が得られる」などの法則（等式）がある。等式を入れると、形の違う木を同じ計算とみなせる。ただし Koka の処理系は、ハンドラーが法則を満たすかを一般には証明しないので、必要なら仕様やテストで確かめる。
自由モデルからモナドへ
圏、関手、自然変換、モナド、随伴を駆け足で説明したうえで、自由モデル関手と忘却関手が随伴をなし、その合成がモナドになることを示す。Haskell のフリーモナドは operation の木をそのままデータとして持つので、等式で同じとされる木も区別する点が自由モデルと違う。
ハンドラーと合成
論文では、ハンドラーは等式理論の（自由とは限らない）モデルに対応し、ハンドリングは自由モデルの普遍性から得られる一意な準同型として与えられる。エフェクトの合成は提唱者の基本構図の外にある話で、実装側ではモナド変換子、フリーモナド、Extensible Effects が、理論側では Graded Monad などが別々に発展してきた。