はじめに

これは前回の続きであり､型 Advent Calendar 2019の8日目の記事で､触れられなかった多相なエフェクトについてです｡

一瞬出てきた多相なエフェクトの例を見てみましょう｡

type 'a option = Some of 'a | None

effect Option : 'a option -> 'a

let with_option = handler
  | effect (Option (Some v)) k -> k v
  | effect (Option None)     _ -> None
  | val v -> v

まずはエフェクトの定義をじっと眺める｡

effect Option : 'a option -> 'a

'a optionを受け取って継続に'aを渡すという型である｡'aという型変数で全称量化されているので多相エフェクト｡

ハンドラwith_optionは'a option -> ('a -> 'b) -> 'b のようにコンストラクタを剥がしてくれる｡そしてNoneが渡された場合にはNoneをそのまま返す｡前回の内容に沿うと､ハンドラの型は

val with_option : 'a!{Option} => ('a option)!{}

となる｡すなわち､

let return v = Some v in
let op v = perform (Option v) in
with_option
  let x = return 3 in
  let y = return 5 in
  return (string_of_int (op x + op y))
  (* ==> Some "8" *)

Option Monadライクなことができる｡

ところでint optionの中身のintをどうにかすることを考える｡

let with_add5_option = handler
  | effect (Option (Some v)) k -> k (v + 5)
  (* ... *)

実はこのコードは問題がある｡たとえばtを返しつつOptionエフェクトが発生する式の型はt!{Option}となり､実際にOptionエフェクトに渡される'a optionの'aは何型なのか情報がない｡つまりハンドラでは'a optionの'aに放り込まれる型情報を使えないため､上記のように具体的な型(int)を使ったコードは書けない｡お手元のMulticore OCamlやEffでwith_add5_optionのような関数を書くとコンパイラが怒ってくる｡

4.06.1+multicoreに起こられる例

# let with_add5_option th =
    match th () with
    | effect (Option (Some v)) k -> continue k (v + 5)
    (* ... *)
Error: This expression has type effect but an expression was expected of type
         int
(* `'a` が `effect` という型名にunifyされている *)

polymorphic effects and parameterized effects

他にも多相なエフェクトのデザイン方法がある｡

effect 'a Option : 'a option -> 'a

KokaやLinksなどではこのように､型変数がエフェクトの引数の外側にある､つまり'aでパラメタライズされている｡このような多相なエフェクトの表現方法を parameterized effects と呼ぶ｡一方､これまでに紹介してきた､Effなどの多相なエフェクトの定義を polymorphic effects と呼ぶ｡

parameterized effectsなら上記のようなハンドラ内で具体的な型の実装ができそうだ｡

val with_add5_option : 'a!{int Option} -> ('a option)!{}

たとえばparameterized effectsを採用しているKoka言語ならOK

effect option<a> {
  fun option(v : maybe<a>): a
}

val with_add5_option : forall <a> (() -> <option<int>> maybe<a>) -> maybe<a>
= handler {
  option(m) -> match(m) {
    Just(v) -> resume(v + 5)
    Nothing -> Nothing
  }
  return x -> x
}

他にも､continuation monadのエミュレーションはparameterized effectsではできますがpolymorphic effectsではできません｡

Multicore OCamlによる実装(RTEする) https://gist.github.com/Nymphium/01619c1c63595afef20ae35984680358
Kokaによる実装(well-typed) https://gist.github.com/Nymphium/3632858aa979d97a07f113ec0a7f629f

おわりに(未完)

row-based effect systemとかに話をつなげていきたかったが筆者の認識が間違いまくってたので文献を見直す必要があるのでまた今度…｡

参考文献

このあたりを読むと本記事で本来書かれるはずだった内容が分かります｡

Sekiyama, Taro, and Atsushi Igarashi. "Handling polymorphic algebraic effects." European Symposium on Programming. Springer, Cham, 2019.
Kammar, Ohad, and Matija Pretnar. "No value restriction is needed for algebraic effects and handlers." Journal of Functional Programming 27 (2017).
Leijen, Daan. Algebraic Effects for Functional Programming. Technical Report. 15 pages. https://www.microsoft.com/en-us/research/publication/algebraic-effects-for-functional-programming, 2016.