Desk言語とAlgebraic Effects and Handlers（代数的エフェクト）

言語実装 Advent Calendar 2022の4日目の記事です。

Desk言語は代数的エフェクト（Algebraic Effects and Handlers）を搭載した言語です。本記事ではDesk言語のeffectについて深ぼって説明します。

Desk言語ではeffectというものを使って副作用を表現します。逆にeffectがないと一切の副作用を表現できません。
また、Desk言語だけでは副作用を実現できないため、effectをシステムコールのように扱って外部リソースとやりとりします。
effectは型システムによって推論され、型を見るだけで、その式がどのような副作用を持つかがわかります。

代数的エフェクト

代数的エフェクトについてはこちらの論文を読んでください。

……だけだとちょっと不親切なので、ざっくり言うと、エフェクトとはReact Hooksです^[1]！
effectという単一のシンプルな言語機能だけで、例外・モナド・async/await・コルーチン・非決定的な計算など様々なものを表現できます。

他に簡単な解説記事もありますが、本記事の方が、早く簡単に代数的エフェクトを理解できることを目指したので、この記事だけ読めば大丈夫です^[2]。

Effect

effectは $\tau_1 \, \leadsto \, \tau_2$ と表現されます（以後 $\tau$ や $\tau_1$ などは任意の型を表します）。
矢印の左側（上でいう $\tau_1$）をエフェクトの「入力」と呼び、右側（上でいう $\tau_2$）をエフェクトの出力と呼びます。
つまり、Desk言語において、副作用は全て入力と出力を持ちます。また、副作用の区別は入力と出力の型によってなされます。

実際にeffectを起こすことをperformと呼びます。以下のように! expr ~> typeがperform式です。

! 1 ~> 'string

1を入力にeffectを発火（perform）しています。
ちなみに、このeffectは $\texttt{'integer} \, \leadsto \, \texttt{'string}$ です。

いろいろなEffect

例を見る方が早いのでいろいろなeffectの例を見てみましょう。

print （文字列の表示）

$$\texttt{'string} \, \leadsto \, \texttt{@"printed"} \, \texttt{*<>}$$

これがprintです。入力が $\texttt{'string}$ で出力が $\texttt{@"printed"} \, \texttt{*<>}$ です。
$\texttt{@"printed"}$は型に付けるラベルで、$\texttt{*<>}$は空のタプル（Rustでいう()）です。Rustに近い見た目で書くと以下のようになるでしょう。

print: &str ~> Printed<()>

文字列を受け取って()を返すのでprintln!に似ていますね。実際それと同じような動作をします。

get/set （状態の取得と保存）

$$\texttt{*<>} \, \leadsto \, \texttt{+<} \, \texttt{@"state"} \, \tau \, , \texttt{@"none"} \, \texttt{*<>} \texttt{>}$$

これがgetで、

$$\texttt{@"state"} \, \tau \, \leadsto \, \texttt{*<>}$$

これがsetです。

それぞれRustっぽく書くと以下のようになります。

get: () ~> enum { State(T), None }

set: State<T> ~> ()

$\texttt{+<}...\texttt{>}$ がenumに相当します。enumが突然出てきて驚かれたかもしれませんが、Desk言語は型を事前に定義するという概念がないので、Rustに直すと上のようになってしまいます。

getにしてもsetにしても入力や出力が直感的だと思います。Desk言語のEffectシステムは直感的に扱えそうだなと思っていただけていたら大成功です。

補足ですが、このget/setはストレージを選ばず使うことができます。なぜなら「アプリのグローバルステート用のhandler」や「スレッドローカルストレージ用のhandler」などを後から自由に指定できるからです（handlerについては後述します）。逆に、コード上でストレージを区別したい場合は@"state"を@"global state"や@"thread local storage"と書き換えるだけです。

throw （例外）

$$\texttt{@"exception"} \, \tau \, \leadsto \, \texttt{*<>}$$

これはもう説明なしで読めるのではないでしょうか？例外オブジェクトが入力で$\texttt{*<>}$が出力です。
なんとなく直感的な気がすると思いますが、違和感を感じている方もいると思います。
違和感の原因は「出力」があるからだと思います。一般的に例外は投げっぱなしにして、だれかに例外処理を一任します。となると「出力」っぽいものはどこにもないです。
Desk言語のeffectは必ず出力を持ちます。かつ、Desk言語で例外を表すにはeffectを使います。「入力」は例外オブジェクトです。では「出力」はなにを表すのでしょうか？この問いについてはあとで解説するので一旦無視してください。

また、まだ例外を処理する話はできていません。throwとcatchはセットのはずです。実際、Desk言語でもそれはセットになっていて、前者はeffectであり、後者はhandlerです。
というわけで、次はhandlerの話をします。

Handler

handlerは特定のeffectを処理するものです。以下はDesk言語でそれを行うための（コンパイル可能な）コードです。

'handle ^Effectを含む関数(*<>) {
  'string ~> @"printed" *<> => <~! @"printed" *<> ~> *<>,
  @"ゼロ除算" 'integer ~> 'integer => "ok",
}

Rustっぽく書くとこうです。

handle Effectを含む関数(()) {
  &str ~> Printed<()> => continue Printed<()> ~> (),
  ゼロ除算<i32> ~> i32 => "ok",
}

説明していない構文をたくさん出してしまいましたので、一気に説明します。

^Effectを含む関数(*<>)はEffectを含む関数という型の関数を、Rustでいう*<>を引数に呼び出しています。Desk言語は引数を持たない関数を作れないのでそのような場合はこの例のように明示的に*<>を受け取る関数にする必要があります。

'handle expr { effect => expr, ... }がhandle式です。
この例では $\texttt{'string} \, \leadsto \, \texttt{@"printed"} \, \texttt{*<>}$ というeffectと $\texttt{@"ゼロ除算"} \, \texttt{'integer} \, \leadsto \, \texttt{'integer}$ というeffectとの2つを処理しています。
前者は先ほどでてきた、printですね。後者はなんとなくわかると思いますが、ゼロ除算例外です。例外なのにここにも出力がありますね。しかも $\texttt{*<>}$ ではありません。

<~! expr ~> typeはcontinue式です。実は!（perform式）を使っても同じことを書けますが、便利なのでこちらを使うことが多いです。!を使う方法も後で説明します。

以上で構文上の説明は終わりです。実際にこのプログラムがどのように動作するかを考えてみます。

まず、handle式で呼び出した関数は２種類の副作用を持つようです。たぶん関数の型は以下のようになっているでしょう。

$$\backslash \, \texttt{*<>} \, \rightarrow \, \texttt{!} \, \{ \\ \texttt{'string} \, \leadsto \, \texttt{@"printed"} \, \texttt{*<>}, \\ \texttt{@"ゼロ除算"} \, \texttt{'integer} \, \leadsto \, \texttt{'integer} \\ \} \, \texttt{*<>}$$

おっと、驚かせてしまいました。まずはeffectを無視した型を見てみます。

$$\backslash \, \texttt{*<>} \, \rightarrow \, \texttt{*<>}$$

とてもわかりやすいですね。Rustだとこうです。

fn(()) -> ()

もとの型に戻ってみると、違いは! { ... }の部分ということがわかると思います。これは式がperformする可能性のあるeffectの集合になっており、これは型システムにより推論されます。
このような型になっていることから、関数の内部に ! "hello world" ~> @"printed" *<> や ! @"ゼロ除算" expr ~> 'number といった式があることを想像できます。

ではまず関数内で! "hello world" ~> @printed *<>が呼ばれた時には何が起こるでしょうか。上のhandle式を見ながらすこし考えてみてください。

正解は「何も起こらず、関数内の処理がそのまま続く」です。関数側はprintすることを想定してeffectをperformしましたが、handlerでは何も出力しないままに、<~ @"printed" *<> ~> *<>でEffectに対して出力を渡して、処理を継続（continue）させています。
effectは $\tau_1 \, \leadsto \, \tau_2$ と表現されると説明しましたが、これはインターフェースのようなものであり、このインターフェースに則っていればこの例のようにhandlerは何でもいいというのが、Algebraic Effects and Handlersの特徴といって良いでしょう。

次に関数内で! @"ゼロ除算" 1 ~> 'numberが起こったら何が起こるでしょうか。こちらも上を参照しながら考えてみてください。

こちらの正解は「関数の実行が完全に中断されて、handle式の評価値が"ok"になる」です。こちらでは<~（continue式）を使いませんでした。そのため、関数はeffectの発生時点で処理が止まり、そのままhandle式全体の評価に移り、"ok"と評価されるわけです^[3]。

なぜ例外に「出力」が必要なのか

以上の話で、なぜDesk言語の例外に出力が必要なのかがわかった方もいると思います。ざっくり言えば、Desk言語のeffectはcontinue（継続）できるからです。Desk言語ではeffectを「入力」とともにperformすることができ、handlerから「出力」を受け取ることで処理をcontinueすることができます。

つまり例外もcontinueできるということです。
試しに実際にやってみましょう。

'handle ^ゼロ除算を含む関数(*<>) {
  @"ゼロ除算" 'integer ~> 'integer => <~! 0 ~> *<>,
}

こうするとゼロ除算が起きたとしても、例外による失敗はしなくなり、3 / 0のような計算の結果は（effectの出力である）0になります。

PerformとContinueは対称

continue式の代わりにperform式が使えると、先ほど説明しました。その例をお見せします。

'handle ^Effectを含む関数(*<>) {
  'string ~> @"printed" *<> => ! @"printed" *<> ~> *<>,
}

こちらもコンパイルが通り、期待通り動きます。先ほどとの違いは<~!を!に変更しただけです。

はいそうです、performとcontinueは対称です。つまり「effectに対して、ある値を出力として渡してcontinueさせること」＝「ある値を入力としてperformしてhandle対象の式の評価された値を出力として受け取ること」となります。

<~!を!にするだけなので、タイプ数が減りましたね。しかし、基本的には<~!を使いましょう。continueしていることをコードを読む人に対して明示できるだけでなく、間違ってcontinueとは関係ない別のeffectをperformしてしまっていないかをコンパイラが検査してくれます。

逆に!を使ってcontinueしないといけない場面はなんでしょうか。実は<~!はhandle式の中でしか使えません。従って、外部でhandlerを定義したいときは!を使う必要があります。

'forall output \ *<> -> ! { @"ゼロ除算" 'number ~> output } *<>

このように多相を用いれば、どんな型を返す式に対しても同じhandlerを使い回すことができます。

Multi-shotな継続

Desk言語ではeffectに出力を渡して処理をcontinueさせることができると説明しましたが、実は出力は何度でも渡すことができます。以下の例を見てみましょう。

'type add \ *<@1 'number, @2 'number> -> @sum 'number
'handle 'begin
  $ ! "a" ~> 'number;
  ^add(&'number, &'number)
'end {
  'string ~> 'number =>
    ^add(<~! 1 ~> 'number, <~! 2 ~> 'number)
}

ちょっと複雑ですね。Rustっぽく書き直してみましょう。

handle {
  let number = ! "a" ~> i32;
  number * 2
} {
  'string ~> 'number => (<~! 1 ~> i32) + (<~! 2 ~> i32)
}

このコードでは"a"を入力にしてeffectを発生させ、その出力を2倍しています。
また、handlerでは2回continueして、その2回の出力を足しています。

さてこの式全体の結果は何になるでしょうか。少し考えてみてください。

答えを説明します。1と2でcontinueしたことと同じことをコードの変形で同じ結果になる式に置き換えてみましょう。

(<~! 1 ~> 'number) + (<~! 2 ~> 'number)

このように2回continueしていました。これを

(1 * 2) + (2 * 2)

と変形するのと同じ結果になります。

つまり結果は6となります。

Effectとはシステムコールである

実はDesk言語単体では副作用のあるプログラムを書けません。いくらDesk言語内でうまくeffectを使おうとしても、ファイルを読み書きしたり、現在時刻を取得したり、軽量プロセスを起動したりといったことはできないわけです。

しかし1つだけ、Deskのプログラムにそういった副作用を持たせる方法があります。それはeffectを外界とのインターフェースとして扱い、他の言語でシステムコールを呼ぶような感覚でeffectをperformし、言語処理系（DeskVM）が適切にeffectを処理すれば良いわけです。
つまり、言語内で解決できるeffectは「言語内のhandler」を使い、本物の副作用を扱いたい場合は「言語外のhandler」を使うことになります。

ところで、型システムにより、静的に全てのシステムコールを列挙できるわけですが、セキュリティー的に良いと思いませんか？

Appendix 1. 高階関数とEffect

高階関数、例えばmapはどのような型になるでしょうか。

$$\texttt{'forall a} \, \texttt{'forall b} \, \texttt{'forall t:} \, \backslash \texttt{a} \, \rightarrow \, \texttt{b} \\ \backslash \texttt{t} \, \rightarrow \, \backslash \texttt{[a]} \, \rightarrow \, \texttt{!} \, \texttt{\^{}} \, \texttt{t(a) [b]}$$

! ^t(a) [b]のところ以外は読めると思います。
^t(a)はt関数にaという引数を渡した時に起こる可能性のあるeffectの集合を意味します。
map関数にeffectfulな関数を渡したとしてもちゃんと結果の型にeffectが表れます。

!の後の部分はeffect exprと呼ばれるものを置くことができて、前述の{effect, ...}や^t(a)以外にも-<effect expr, effect expr>（effect集合の減算）や+<effect expr, ...>（effect集合の加算）のようなものがあり、様々な高階関数にeffectが正しく推論できる型付けをすることができるようになっています^[4]。

実装の話をすると、この辺りはテストケースや実装が足りてなくて、おそらくうまく動かないので、どなたかテストと実装を手伝っていただけると嬉しいです。

Appendix 2. Effectの推論

perform式を含む式は $\texttt{!} \, \{ \texttt{effect, ...} \} \, \tau$ と型付けされます。
関数のbodyが $\texttt{!} \, e \, \tau$ のとき関数の型は $\backslash \, \tau_1 \, \rightarrow \, \texttt{!} \, e \, \tau$ となります。
handle式について、対象の式のeffectの集合を $e_{target}$ 、処理されたeffectの集合を $e_{handled}$ 、各handlerについて、handler1のeffectの集合を $e_{handler1}$、handler1のcontinueのeffectだけを含む集合を $e_{continue1}$ とするとき、handle式のエフェクト集合は以下のようになる。

$$\texttt{let} \, e_{remain} = e_{target} - e_{handled};\\ \texttt{let} \, e_{handler1remain} = e_{handler1} - e_{continue1};\\ \texttt{let} \, e_{handler2remain} = e_{handler2} - e_{continue2};\\ e_{remain} + e_{handler1remain} + e_{handler2remain} + ...$$

詳しくはtypeinferの実装を読んでください。

脚注

1. 怒られそう

2. 一応リンクhttps://overreacted.io/ja/algebraic-effects-for-the-rest-of-us/

3. 当然ですがこのhandle式の型は+<'string, *<>>と推論されます

4. この型システムのsoundでcompleteなのかどうかはいずれ証明してみたい