代数的演算 (algebraic operations)

type-theory programming-paradigm

副作用を「代数的理論(演算の signature + 等式)の演算」としてモデル化する考え方。Plotkin & Power の理論で、Algebraic Effects の「代数的」が何を指すかの正体。効果が「代数的演算」だからこそ、ハンドラがその「解釈」になり、モナドと繋がる。

演算は「継続を引数に取る」形をしている

各副作用を、結果の続き(継続)を引数に取る演算として書く(generic effects)。

効果	演算の型	読み
状態 get	`get : (S → X) → X`	状態を読んで続きへ渡す
状態 put	`put : S × X → X`	状態を書いて続きへ
非決定 choose	`choose : X × X → X`	2つの続きに分岐
例外 raise	`raise : X` (0引数=空)	続きが無い(脱出)

ポイントは演算が計算 X を引数・結果に持つこと。raise が0引数(arity 0)なのは「続きが無い=戻らない」を表す。[effect-handlers|継続の resume 回数]はこの arity と対応する。

「代数的」= 等式で意味を縛る

演算には等式 (algebraic theory) が課される。例えば状態の法則:

get (λs. put s k)        = k                 -- 読んだ値をそのまま書くと無変化
put s (get (λs'. k s'))  = put s (k s)       -- 書いた直後に読むと書いた値
put s (put s' k)         = put s' k          -- 連続 put は最後だけ効く

この等式系(= Lawvere theory / 代数的理論)が「状態とは何か」を意味として定義する。演算 + 等式で代数を作るから「代数的」。

自由モデルとは

理論のモデル(代数) = 台集合 + 各演算の解釈で、課された等式を満たすもの。集合 X 上の自由モデルは、X を葉・演算を節にした項(木)を、課された等式だけで割ったもの。“自由” = 要求された等式以外の同一視を一切しない(余計な関係を勝手に足さない)= 実質「構文そのもの」。

理論	生成集合	自由モデル
モノイド	アルファベット `A`	リスト `[A]`(連結・単位だけ。`ab ≠ ba`)
群	生成元	既約語
代数的効果の理論	戻り値 `X`	効果の構文木(get/put/… の木、葉が `X`)

普遍性(これがハンドラの正体) — X から任意のモデル M への写像 X → M は、自由モデルからの準同型 T X → M に一意に延びる(圏論では「忘却関手の左随伴」)。

→ つまり 戻り値の解釈 X → M + 各演算の解釈(= モデル M)を与えれば、プログラム全体の解釈が一意に決まる。これがハンドラ = 自由モデルから別モデルへの準同型、ということ。

自由モデル → 自由モナド

効果理論の X 上の自由モデルを、X について関手と見たものが 自由モナド T X(= 副作用プログラムの AST)。だから代数的効果とモナドが理論で繋がる。ハンドラはこの T X から「自由でない」別モデルへ落とす解釈にあたる。

何が代数的に表せるか(線引き)

「代数的」であるには、演算が継続に対して一様(可換)に振る舞う必要がある。

代数的: 状態・例外・非決定・入出力 → 効果ハンドラで素直に扱える
非代数的(この枠に素直に乗らない): call/cc のような継続そのものを捕まえる操作、一部の higher-order な効果。これらは別扱い(Plotkin-Pretnar の handler や後続研究が拡張を議論)

この線引きが「どの副作用が algebraic effects で扱いやすいか」を決めている。

押さえどころ（カード化候補）

代数的演算とは → 副作用を「代数的理論(演算 signature + 等式)の演算」でモデル化する考え(Plotkin & Power)。algebraic effects の「代数的」の中身。
演算の形 → 継続を引数に取る(generic effects)。get:(S→X)→X、raise:X(arity 0=戻らない)。arity が継続の resume 回数に対応。
等式で意味を定義 → put-put / put-get 等の法則(Lawvere theory)が「状態とは何か」を縛る。演算+等式だから「代数的」。
自由モデルとは → 演算で組んだ項を「課された等式だけ」で割った最も自由なモデル(余計な同一視をしない=構文そのもの)。自由モノイド=リストの効果版。
普遍性=ハンドラ → X→M(戻り値の解釈)が自由モデルからの準同型 T X→M に一意に延びる。「葉の解釈+演算の解釈を決めれば全体が一意」がハンドラの成立理由。
自由モデル=自由モナド → 自由モデルを関手と見たものが自由モナド T X(=副作用 AST)。代数的効果と Monad が繋がる所以。
線引き → 状態/例外/非決定/IO は代数的、call/cc 等は非代数的。これが扱いやすさの境界。