effect system勉強会
2019-05-26＠サイボウズ、主催びしょ〜じょさん。
Extensible Eff Applicative
Applicativeの話。
「他の人がモナドの話をすると思ったので、私はアプリカティブの話をします」
Free applicative vs Freer monad
haskelle5 :: FreeAp (Exc String) Integer
e5 = Impure Ap (Exc "foo") $ ImpureAp (Exc "bar") $ Pure (+)
e6 :: Freer (Exc String) Integer
e6 = Impure (Exc "foo") $ \a -> Impure (Exc "bar") $ \b -> Pure (a + b)applicativeの式は"foo"と"bar"両方を参照できる。
monadの式は"foo"のみ取得でき、"bar"を取得するには継続を使うことになる。
free applicativeだと両方取得できるので、たとえばエラーを全て集めるみたいな例だとapplicativeの方が便利。
Free applicativeを拡張可能にしたい。
Extensible Eff Applicative：open unionをfree applicativeに加えたもの。
Eff monadとどうやって共用しよう？
モナドとアプリカティブでプリミティブを分けたくない。
案1：EffApからEffへの変換を書く。
モナドの計算とアプリカティブの計算を型で分けられるけど、いちいち変換しないといけない。
案2：コンストラクタに
Impure も ImpureAp も含めてしまう。使いやすいけど、Applicativeの操作を型で保証できない。
たとえばアプリカティブで並列計算してたところで
flat_map しちゃう、とか。案3：型パラメータに含めてしまう。
これだと弱点は型が複雑になることくらい……？
「この前思いついた所なのでまだあんまり考えられていない」
名前付き extensible effects
fumievalさん
monad transformerだとモナド作るたびにインスタンス作らないといけなくてつらい。
Haskellだとmtl+transformer
のでextensible effectsを使おう。
ただし：
推論されない：型リストからエフェクトの型を定めることができない。
clear :: (Monoid m, State m \in xs) => Eff xs () を作ろうとすると m が曖昧になる。対応できない：同じ方を持つ複数のエフェクトを持てない。
たとえば
[State Int, State Int] からどちらかを意図的に選択することができない。再利用できない：mtlのクラスで定義された演算を再利用できない。
これをHaskellのextensibleというパッケージで解決した。
推論できる：
State m \in xs に当たる制約を Associate "S" (State m) xs みたいに書くことで実現。functional dependencies
"S" は型レベル文字列（DataKinds）対応できる：エフェクトをキーで指定できるのでOK。
再利用できる：mtlのインターフェースが使える。
いちいち手動で再定義する必要は無い。
Effect{ive,ful} Cycle.js
Webフロントエンドのフレームワークは、以下の性質を満たしていてくれると嬉しい。
1. 種々の副作用を互いに分離できる。
異なる副作用は別々に処理したい。
関心の分離をしたい。
テスタビリティを上げたい。
後から副作用を追加できるようにしておきたい。
2. 非同期が織り込み済み。
これを解決するために：
副作用の処理をclient-serverモデルっぽく捉えて、client (DOMとかHTTPとか) が server (effect handler) に副作用 (effect) の処理を依頼する形に考えられないか。
Freer, More Extensible Effectsの図。
→異なる副作用を別々に処理する。
Observable（Stream）を使う。
Observableが値を流し、Observerがその値を使って何をするかを決める。
→非同期が織り込み済み。
Cycle.jsでは、この世界観の元でフロントエンドを書ける。
componentはeffectfulな計算をする。
componentが持つeffectはdriver（やhigher-order component）によってhandleされる。
すべてのeffectをhandleできればアプリケーションが実行できる。
TypeScriptではどこでも副作用を書けてしまうのでアレだが、このフレームワークでは副作用の処理をdriverに書くことで、メインの処理をピュアに書ける。
Cycle.js vs RxJS
Cycle.jsではStreamのライブラリを選べる。なのでStreamとしてRxJSを選ぶこともできる。
Cycle.jsはStreamのラッパー的存在。
Streamの扱い方の指針を与えるフレームワーク
Effective Rust
algebraic effectsをRustに実装した話。
元ネタ：eff.lua
asymmetric coroutineがあればoneshot algebraic effectが実装できる。
Rustにはスタックレスコルーチンがあるので、これを使ってoneshot algebraic effectが実装できる。
pull型で動く。
ハンドラは再開を通知する形。
ランタイムが継続を実行する。
そのまま書くと、Rustのlifetime checkerと相性が悪い。
performで呼ばれるhandlerの中で再びperformを呼びうるが、そうするとふたつのハンドラが同時に参照するので駄目。
Frankという言語で採用してるように、計算と値を区別して、引数の評価中に出たエフェクトを処理する形で書くと良い。
しかもこうすると、エフェクトハンドルがスタックを重ねるスタイルじゃなくてループを回すスタイルになるので速い。
Monads and Effects
モナドから見たeffect systemの話。
注：call-by-value。
そもそもeffectとは。
ここでは：型システムの一種として捉える。
\Gamma \vdash M : A ! e みたいに、judgementにeffect eが付く。
直感：computationをしたときに、高々eというeffectが起きる。
たとえば基本的な型の導出を考えると、どんなeffectの見積もりになりそうか考えてみよう。
たとえば\vdash \langle M_1, M_2 \rangle : A \times B ! ここは何でしょう
他にもletとか関数適用とかラムダ抽象とか。
タプルとletに関しては、「effectがスタックする」みたいなのを考えれば良さそうだ。
例として、memory-state effectを考えてみる。
i番目のメモリセルに書く、読む、みたいな。
いくつかbase effectsがある。
exn : exception div : divergence ndet : non-determinism alloc(h) , read(h) , write(h) : memory operationまた、Kokaではeffectの順番は無視する。
base effectsを組み合わせて色々なeffectを作れる。
total ≡ 〈〉 pure ≡ 〈exn, div〉 st(h) ≡ 〈alloc(h), read(h), write(h)〉 : memory-state h について何でもできるぜ io ≡ 〈st(io), pure, ndet〉 : 何でもできるぜRow-polymorphicっぽくeffectを扱っているのが面白い。
\langle exn | \mu \rangle
ところで、ラムダ抽象と関数適用はどう捉える？
関数の時点では、関数適用のeffectが発生しているとは考えたくない。
代わりに、関数自体にeffectが込められていると考えたい。
ので、関数型の矢印にeffectで添え字を付けて、「関数を呼び出したときにこのeffectが起こりうる」を表現する。
EffectはParametric Monadとして捉えられる。
たとえばHaskellのIOモナドにmemory-state effectが添え字として入ったのをイメージ。
モナドにおけるモナド則的なものはこの場合どういう規則になるだろう？
これを考えると、以下のようなことが分かる。
effectは「スタックする」という演算に対してモノイドになってる。
あくまで上からの見積もりで、preorderが入る。
Further topics
Semantics
Graded monad (for the formal semantics)
Recursion
Algebraic effects and effect handlers
Effect inference
Polymorphic effect
Q.
exn に型パラメーターを入れられる？（たとえばOCamlのexceptionみたいに）A. Kokaには多分無い
Q. たとえば
exn に型パラメーターを持たせると、effect inferenceが多相再帰みたいになって推論不能になったりしそう。Q. effect情報を使ったコンパイルは考えられている？ たとえば
exn が無ければ例外処理消せる、とか。A. Kokaはしてないと思うが、そういう研究はある。たとえば実行にかかるコストをeffectとして見積もるとか。メモリアクセスがdistinctになっている情報がeffectから分かるのでそれを使って並列化可能性を見積もるとか。
How do you implement Algebraic Effects?
びしょ〜じょさん
Algebraic effects and handlerの様々な実装方法について考えたい。
低レベルで実装する。
例：libhandler。Cで実装されたライブラリ。
effect invocation ： longjmp
effect handler ： stackframe + ip
continuation ： stackframe + ip
様々な言語から呼び出せて速いけど、実装が大変。バックエンド向け？
コルーチンで実装する。
effect invocation ： yield
effect handler ： create & resume
continuation ： coroutine
ただしcoroutineをコピーするような操作が無いと、continuationがoneshotに限定される。
continuationは何回も呼び出したいものなのに、coroutineは状態をコピーできない。
Multiprompt shift/resetで実装する。
例：Effekt
effect operation ： prompt tag
effect invocation ： shift-at
effect handler ： reset-at
continuation ： continuation
Multiprompt shift/reset：普通のshift/resetだとshiftから一番近いpromptまで飛ぶが、multiprompt shift/resetではそれぞれのpromptにタグをつけておくことでshift時に飛びたいpromptを指定できる。
ただしタグはglobalじゃない。
shift-atを重ねるとネストする。
Free monadで実装する。
例：Eff
effect invocation ： Impure
effect handler ： run
continuation ： bindの右辺
N-barrelled CPSで実装する？
Double-barrelled CPS：continuationをふたつ持つ。CPS+exception。
これを拡張して、CPS+algebraic effectsに対応して(1+n)個の継続を持つものを考えれば良いのでは？
この論文と同じ話になるかも？
Effective Idris: Effects
κeenさん
Idrisの標準ライブラリにあるEffectsの話。
idrisEffect : Type
Effect = (x : Type) -> Type -> (x -> Type) -> Type
data EFFECT : Type where
MkEff : Type -> Effect -> EFFECTEffect = 返り値 * リソース * リソースの更新。
Idrisには依存型があるのでリソースが更新されうる。
EFFECT = パラメータ * Effect。
Row-based type systems for algebraic effect handlers
Algebraic effects & handlers: effectのインターフェースと実装を分ける。
handler-not-found errorを事前に防ぎたい。
Row-based effect system (Hillerström+ 2016, ...)
特徴
parametric effectsをrow-polymorphismで扱える。
例：
to-maybe : ∀α. (unit -> <fail> α) -> <> α option このままだと、
to-maybe に与える関数として、effectが fail しか起こらないものしか扱えない。ので、row-polymorphismを使うことで他のeffectがあることを許す。
to-maybe : ∀α. (unit -> <fail | ρ> α) -> <| ρ> α option 型上でeffectの複製ができる。
<fail, int choose, fail> とか書ける。 <int choose, bool choose> みたいに書いて、ハンドラでは int choose -> ... みたいに書ける。ただしこう書くと順番があって、先に
int choose をハンドルしないといけない。この仕組みがあるとsubtypingが無くても結構リッチな型が書けるのでeffect systemが単純になる。
effectの抽象化がやりやすくなる。
continuationと機能としては似ているのだけど、effect systemという側面から見ると面白さがあって良さ。
OCamlのラベル引数の体系は「名前が違うと順番は気にしないが、名前が同じだと順番を気にする」という意味で似てる、という話。
懇親会
僕「oneshotのalgebraic effectってどのくらいデメリットあるんですか」
multishotであってほしいものって、リストにmapするときのfとか、非決定的に何回か計算が必要なときとか。
要するに任意回必要な場合。
なので、使い方によってはoneshotであまり困らない。
ややポジショントークかもしれない。
こういうのはoneshot制約がかかっている論文には（査読を通すために）色々書いてあるので読むと良い。
ファイルをreadして、closeをちょうど1回だけしたいときとか、oneshotの方がたすかることもある。
これはポジショントークっぽい。
線形型やアフィン型で解決したい問題っぽい。
algebraic effectを継続だと思うと、継続が役に立つ場面であるバックトラックをする場面では、oneshotだと困る。
effectをpolymorphicにするときに、effectの方に型変数をつけるか、effectの型の方に型変数をつけるかでeffect推論の難易度が変わる。
正確には、型アノテーションをつけるかつけないか？
∀α. α e :: α → α と e :: ∀α. α → α 後者だと
handle :: Λα. ... って感じでハンドラの中で型を受け取って色々することになる。だからハンドラの中では
(+) とか使えない。let-polymorphismにvalue restrictionが必要なのと同じように、そのままやると推論が壊れる。
value restrictionが無くても、ハンドラのbodyを制限すると上手くやれるよって話。