前回の記事に「例外は限定継続の上に乗っける感じで実装するべきなのかもしれません」と書きました。この記事では、その辺の話を掘り下げ、「Representing Monads」に繋げます。
限定継続による例外の試み
例外とは大域脱出とそれを捕捉する機構です。エラーの種類を表す情報として、Standard MLでは exn
型の値を受け渡しできます。
大域脱出および exn
型の値の受け渡しは、ML上のmulti-promptな限定継続の言葉で書けば、
val exnPrompt : exn prompt = newPrompt () val abort : 'a prompt * 'a -> 'b (* exn prompt * exn -> 'b として使う *)
というプロンプトとabort関数を使えば実現できそうです。例外の送出を行う関数(SMLのraiseに相当)は
fun myraise (e : exn) = abort (exnPrompt, e)
となるでしょうか。「割る数が0の場合にこの独自の例外機構を使って Div
例外を投げる除算関数」 mydiv
は次のように実装できます:
fun mydiv (x : int, y : int) = if y = 0 then myraise Div else x div y
例外をキャッチする部分はどうなるでしょうか。abortの飛び先はpushPrompt(shift/resetのresetに相当)なので、pushPromptしてみます。
(* val pushPrompt : 'a prompt * (unit -> 'a) -> 'a *) val result = pushPrompt (exnPrompt, fn () => ...処理...) (* result は飛んできた例外 *)
「処理」の部分で常に例外が飛ぶのであればこれで良いのですが、「例外」が飛ぶのは例外的な状況です。大抵は正常終了して、 exn
型とは限らない何らかの値が返ってきます。
仮に、「処理」の正常終了時の結果の型が int
だとしましょう。すると、 result
は int
(正常終了時)か exn
(例外発生時)のどちらかを表す型(直和型)でなくてはなりません。そういう直和型を定義してみましょう:
datatype 'a result = OK of 'a | ERROR of exn val exnPrompt : (int result) prompt = newPrompt (); fun myraise (e : exn) = abort (exnPrompt, ERROR e); fun mydiv (x, y) = ... val result : int result = pushPrompt (exnPrompt, fn () => (...処理...; OK 42)); case result of OK x => x | ERROR e => ...例外の処理(ハンドラー)...
この際、プロンプトの型も int result
である必要があります(なんだか雲行きが怪しくなってきましたね)。
さて、例外ハンドラーはネストすることができます。次のコードでは、1 div 0
で出る(この例だと出ませんが)Overflow
例外を内側の handle
でキャッチし、 Int.toString (...)
で出る Div
例外を外側の handle
でキャッチしています:
Int.toString (1 div 0 handle Overflow => 999) handle Div => "div by zero"
この例を自作例外機構で実装してみましょう。
val result = pushPrompt (exnPrompt, fn () => OK (Int.toString (case pushPrompt (exnPrompt, fn () => OK (mydiv (1, 0))) of OK x => x | ERROR Overflow => 999 | ERROR e => myraise e))); case result of OK x => x | ERROR Div => "div by zero" | ERROR e => myraise e
……残念なことに、これはコンパイルが通りません。内側のpushPromptは型が合っているのですが、外側のpushPromptの型が合わないのです(exnPromptの型により中の関数は int result
を返さなければならないが、実際には string result
が返ってくる)。
型のない言語であればこれは問題にはなりません。上記に相当するコードを問題なく実行できるはずです。
あるいは、TypeScriptのように「なんでも突っ込める型」 any
があればプロンプトの型を (any result) prompt
とすることで自作の例外機構が実現できたでしょう。
はい、というわけで型システムを迂回する手段の登場です。以下のようなインターフェースを持ったストラクチャーを用意しましょう:
structure Universal :> sig type u (* なんでも突っ込める型 *) val to_u : 'a -> u val from_u : u -> 'a (* 不変条件:from_u (to_u x) = x *) end
LunarMLのJavaScriptバックエンドではこのストラクチャーは次のように実装できます:
structure Universal = struct type u = JavaScript.value val to_u = Unsafe.cast val from_u = Unsafe.cast end
思いっきり型システムを迂回してますね。実はSMLの場合は型システムを迂回しなくても同等のことはできますが、それは後で。
この Universal
を使うと、先ほどの例は次のような型チェックの通るStandard MLコードとして書けます:
val exnPrompt : (Universal.u result) prompt = newPrompt () fun myraise (e : exn) = abort (exnPrompt, ERROR e) fun mydiv (x : int, y : int) = if y = 0 then myraise Div else x div y val result = pushPrompt (exnPrompt, fn () => OK (Universal.to_u (Int.toString (case pushPrompt (exnPrompt, fn () => OK (Universal.to_u (mydiv (1, 0)))) of OK x => Universal.from_u x | ERROR Overflow => 999 | ERROR e => myraise e)))); print (case result of OK x => Universal.from_u x | ERROR Div => "div by zero" | ERROR e => myraise e);
実行例:
$ ./lunarml --js-cps exntest.sml $ node exntest.js div by zero
例外をハンドルする部分を関数に追い出すと
fun myhandle (computation : unit -> 'a, handler : exn -> 'a) : 'a = case pushPrompt (exnPrompt, fn () => OK (Universal.to_u (computation ()))) of OK x => Universal.from_u x | ERROR e => handler e; print (myhandle (fn () => Int.toString (myhandle (fn () => mydiv (1, 0), fn Overflow => 999 | e => myraise e)), fn Div => "div by zero" | e => myraise e));
となります。
モナドへ
ここまでの例は、限定継続によって例外についてのモナド(Haskellで言うところの Either e
モナド)を実装したと言えそうです。
また、非決定的計算を表すリストモナドっぽいものは限定継続の使用例として前回の記事で紹介しました。
他のモナドについてはどうでしょうか。
実は、純粋関数で(unitとbindを)表現できる任意のモナドは限定継続(と、「なんでも突っ込める型」Universal)で実装できるというのが次の論文で示されています:
- Andrzej Filinski. 1994. Representing monads. In Proceedings of the 21st ACM SIGPLAN-SIGACT symposium on Principles of programming languages (POPL ’94). Association for Computing Machinery, New York, NY, USA, 446–457. https://doi.org/10.1145/174675.178047
純粋関数で表現できるモナドの例としては、例外やリストモナドの他に、Readerモナドや状態モナド、それから継続モナドも含まれます。
限定継続ってすごいな!?
この論文に出てくる例をLunarMLで実装したものは
に置いてあります。
SML/NJやMLtonは限定継続ではなく大域的な継続を提供しています。Representing Monadsでは大域的な継続(call/cc)と一個の可変なグローバル変数から限定継続を実装する方法も示しているようです(←読んでない)。
補遺:Universalストラクチャーについて
本文中のUniversalストラクチャーはRepresenting Monadsに登場したものですが、それとは少し違う「なんでも突っ込める」UniversalストラクチャーがSMLのBasis Libraryに最近追加(提案?)されています。元ネタはPoly/MLのもののようです。
structure Universal : sig type universal type 'a tag val tag : unit -> 'a tag val tagInject : 'a tag -> 'a -> universal val tagIs : 'a tag -> universal -> bool val tagProject : 'a tag -> universal -> 'a end
違いは、タグを明示的に作るようになったことです。このストラクチャーは純粋なStandard MLで実装することができ、実装例は
structure Universal :> sig type universal type 'a tag val tag : unit -> 'a tag val tagInject : 'a tag -> 'a -> universal val tagIs : 'a tag -> universal -> bool val tagProject : 'a tag -> universal -> 'a end = struct type universal = exn type 'a tag = { project : exn -> 'a, inject : 'a -> exn } fun tag () : 'a tag = let exception T of 'a fun project (T x) = x | project _ = raise Match in { project = project, inject = T } end fun tagInject { project, inject } = inject fun tagIs { project, inject } u = (project u; true) handle Match => false fun tagProject { project, inject } = project end;
となります。こっちのUniversalストラクチャーを使うと、限定継続による例外処理は
val exnPrompt : (Universal.universal result) prompt = newPrompt () fun myraise (e : exn) = abort (exnPrompt, ERROR e) fun myhandle (computation : unit -> 'a, handler : exn -> 'a) : 'a = let val tag = Universal.tag () in case pushPrompt (exnPrompt, fn () => OK (Universal.tagInject tag (computation ()))) of OK x => Universal.tagProject tag x | ERROR e => handler e end;
と書けます。
あるいは、どうせexceptionを動的に作るのであれば
val exnPrompt : exn prompt = newPrompt () fun myraise (e : exn) = abort (exnPrompt, e) fun myhandle (computation : unit -> 'a, handler : exn -> 'a) : 'a = let exception OK of 'a in case pushPrompt (exnPrompt, fn () => OK (computation ())) of OK x => x | e => handler e end;
としてしまって良いかもしれません。
ピンバック: 限定継続いろいろ | 雑記帳