Help us understand the problem. What is going on with this article?

Algebraic Effectsの型システム入門(2) 多相エフェクト

はじめに

これは前回の続きであり、型 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ではできません。

おわりに(未完)

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

参考文献

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

Why not register and get more from Qiita?
  1. We will deliver articles that match you
    By following users and tags, you can catch up information on technical fields that you are interested in as a whole
  2. you can read useful information later efficiently
    By "stocking" the articles you like, you can search right away
Comments
Sign up for free and join this conversation.
If you already have a Qiita account
Why do not you register as a user and use Qiita more conveniently?
You need to log in to use this function. Qiita can be used more conveniently after logging in.
You seem to be reading articles frequently this month. Qiita can be used more conveniently after logging in.
  1. We will deliver articles that match you
    By following users and tags, you can catch up information on technical fields that you are interested in as a whole
  2. you can read useful information later efficiently
    By "stocking" the articles you like, you can search right away