Dive into Algebraic Effects
びしょ〜じょML Days #2

September 16, 2018 やること

 Algebraic Effects を伝道
Algebraic Effects is 何 Algebraic Effects が使える言語
Algebraic Effects の活用事例

研究のご紹介
先日 JSSST でポスター発表した内容を紹介シマス

 目次
自己紹介

Algebraic Effects
effect の型
デモポイント
AE Implimentations

Multicore OCaml
研究紹介
oneshot AE →oneshot s/roneshot s/r → AC
課題、今後の予定
まとめDive into Algebraic Effects

自己紹介

Algebraic Effects
effect の型
デモポイント
AE Implimentations

Multicore OCaml
研究紹介
oneshot AE →oneshot s/roneshot s/r → AC
課題、今後の予定
まとめ 自己紹介

こんにちは、びしょ〜じょです。

I T 大学大学院で M1 をやっているプログラム言語や型とか検証などの研究室
I 少し前は Lua にお熱だった   Nymphium

自己紹介

1/13

Dive into Algebraic Effects

自己紹介

Algebraic Effects
effect の型
デモポイントAE Implimentations

Multicore OCaml
研究紹介
oneshot AE →oneshot s/roneshot s/r → AC
課題、今後の予定
まとめAlgebraic Effects
イメージとしては継続を持てる例外

Algebraic Effects

2/13

Algebraic Effects
イメージとしては継続を持てる例外
例 (Eff language implementation):
effect Say: string → unit
effect Twice : unit
→ unithandle (perform ( Say " Hello " );perform ( Twice ());
perform ( Say " world " )) with| x → x| effect ( Twice ()) k → k ( ); k ()| effect ( Say msg ) k →print _ endline msg ; k ()Algebraic Effects

2/13

Algebraic Effects
イメージとしては継続を持てる例外
例 (Eff language implementation): effect definition
effect Say: string → unit
effect Twice : unit
→ unithandle (perform ( Say " Hello " );perform ( Twice ());
perform ( Say " world " )) with| x → x| effect ( Twice ()) k → k ( ); k ()| effect ( Say msg ) k →print _ endline msg ; k ()Algebraic Effects

2/13

Algebraic Effects
イメージとしては継続を持てる例外
例 (Eff language implementation): effect definition
effect Say: string → unit
effect Twice : unit→ unit
effect invocation
handle (perform ( Say " Hello " );perform ( Twice ());
perform ( Say " world " )) with| x → x| effect ( Twice ()) k → k ( ); k ()| effect ( Say msg ) k →print _ endline msg ; k ()Algebraic Effects

2/13

Algebraic Effects
イメージとしては継続を持てる例外
例 (Eff language implementation): effect definition
effect Say: string → unit
effect Twice : unit
→ uniteffect invocation
handle (perform ( Say " Hello " );effect handler
perform ( Twice ());
perform ( Say " world " )) with| x → x| effect ( Twice ()) k → k ( ); k ()| effect ( Say msg ) k →print _ endline msg ; k ()Algebraic Effects

2/13

Algebraic Effects
イメージとしては継続を持てる例外
例 (Eff language implementation): effect definition
effect Say: string → unit
effect Twice : unit
→ uniteffect invocation
handle (perform ( Say " Hello " );effect handler
perform ( Twice ());
perform ( Say " world " )) withcontinuation| x → x| effect ( Twice ()) kk → k ( ); k ()| effect ( Say msg ) k →print _ endline msg ; k ()Algebraic Effects

2/13

•effect の型
なにこれeffect Say : string → unit

Algebraic Effects.effect の型

3/13

•effect の型
なにこれeffect Say : string → unit例:
E [ perform ( Say " Hello " ) ]Algebraic Effects.effect の型

3/13

•effect の型
なにこれeffect Say : string → unit例:
E [ perform ( Say " Hello " ) ]: string

Algebraic Effects.effect の型

3/13

•effect の型
なにこれeffect Say : string → unit例:
E [ perform ( Say " Hello " ) ]: string: unitAlgebraic Effects.effect の型

3/13

•effect の型
なにこれeffect Say : string → unit

例:
: unit → 'a (継続の型)
E [ perform ( Say " Hello " ) ]: string: unitAlgebraic Effects.effect の型

3/13

•effect の型
なにこれeffect Say : string → unit

例:
: unit → 'a (継続の型)
E [ perform ( Say " Hello " ) ]: string: unit

完全に理解した
Algebraic Effects.effect の型

3/13

• デモ
effect Say: string → unit
effect Twice : unit→ unit
handle (perform ( Say " Hello " );perform ( Twice ());
perform ( Say " world " )) with| x → x| effect ( Twice ()) k → k ( ); k ()| effect ( Say msg ) k →print _ endline msg ; k ()Algebraic Effects. デモ

4/13

• ポイント• 定義と実装の分離•
ハンドラの合成• 限定継続が使える

Algebraic Effects. ポイント

モジュラーなプログラミングを支援
例外より強力

5/13

Dive into Algebraic Effects

自己紹介

Algebraic Effects
effect の型
デモポイント
AE Implimentations

Multicore OCaml
研究紹介
oneshot AE →oneshot s/roneshot s/r → AC
課題、今後の予定
まとめAE Implimentations
I Eff*1• ML ベースの syntax、型推論• 処理系やライブラリ (EDSL) など実装多数

I Koka*2• MS Research 製• effect が型で表される(ex: println ::a::::->::::::::::
console :::())• Algebraic Effects 以外にもおもしろ機能

I Multicore OCaml*3• OCaml Labs が OCaml を fork
• 継続が oneshot の Algebraic Effects を持つ*1

https://www.eff-lang.org/*2

https://koka-lang.github.io/koka/*3

http://ocamllabs.io/doc/multicore.html
AE Implimentations

6/13•Multicore OCaml
State モナド風module State (S : sig type t end )= structtype t = S.t
effect Put : t → unit ;;effect Get : t
let run init f =init |> match f () with| x → ( fun s → (s , x ) )| effect ( Put s ' ) k →( fun s → continue k () s ' )| effect Get k →( fun s → continue k s s )endeffect Log : int → unit
let log msg = perform @@ Log msg
AE Implimentations.Multicore OCaml

try beginlet module S1 =State ( structtype t = intend ) in
let open S1 in
let incr ( ) =perform ( Put ( perform Get + 1))
inrun 0 @@ fun () →incr ( );log @@ perform Get ;incr ( );log @@ perform Get
endwith effect ( Log msg ) k →print _ int msg ; continue k ( )7/13•Multicore OCaml
shift/reset も実装できるぞ!!
module DelimccOne = structtype 'a prompt = {take : 'b. ( ( 'b → 'a ) → 'a ) → 'b ;push : ( unit → 'a ) → 'a ;}let new _ prompt ( type a) : unit → a prompt = fun () →let module M = structeffect Prompt : (( 'b → a) → a) → 'b
end inlet take f = perform (M. Prompt f) in
let push th =try th () with effect (M. Prompt f) k → f @@ continue kin{ take ; push }let push _ prompt { push } = push
let take _ subcont { take } = takelet shift0 p f = take _ subcont p @@ fun k → f k
end
AE Implimentations.Multicore OCaml

8/13

Dive into Algebraic Effects

自己紹介Algebraic Effects
effect の型デモポイントAE Implimentations

Multicore OCaml
研究紹介
oneshot AE →oneshot s/roneshot s/r → AC
課題、今後の予定
まとめ 研究紹介
Asymmetric Coroutine による Oneshot Algebraic
Effects の実装 *4
oneshot shift/reset

1oneshot
Algebraic
Effects2
asymmetriccoroutine(asymmetric) coroutine のある言語で AE が使える
1 の類似の変換、 2 の既存の変換を参考にする*4
http://logic.cs.tsukuba.ac.jp/~sat/pdf/jssst2018.pdf
研究紹介

9/13

oneshot Algebraic Effects → oneshot shift/reset[KS16] に基づき先程の実装の逆をやる
直感としては effect instance→prompt,
effect invocation → shift, effect handler → reset
module Translate (D: DELIMCC ) : sig
type ( 'a , 'b ) free
type 'a thunk = unit → 'aval newi : unit → 'a D. prompt
val op : ( 'a , 'b ) free D. prompt → 'a → 'bval handler : ( 'g , 'g ) free D. prompt →( 'g → 'o ) → ( 'g * ( 'g → 'o ) → 'o ) → 'g thunk → 'oval handle : ( 'a thunk → 'b ) → 'a thunk → 'b
end = struct......
end

Q. 継続の oneshotness を AE が引き継いでることの証明は?
A. まだ無い。 affine type で型によって示す予定
研究紹介.oneshot AE → oneshot s/r

10/13

oneshot shift/reset → Asymmetric Coroutine[Usu17] による変換を使う (Lua による実装)
Lua の coroutine + 現在の thread を表す current※ ただし prompt はない (shift が持つ限定継続は直前の reset)

function sr.reset ( th )local l = coro.create (function (_)
return ( function (y)return function (_ )return y
endend )( th ())
end )return coro.resume (l)()
end

研究紹介.oneshot s/r → ACfunction sr.shift (f)local k = coro.current
return coro.yield ( function ( _)return sr.reset ( function ( )return f(k)end )end )end
function sr.throw (k , e )return coro.resume (k , e )()
end
11/13

• 課題、今後の予定
I oneshotness の保証 (先述)
I Usui による変換の対象の shift/reset をmulti-prompt で再定義
I oneshot shift/reset を経由しないダイレクトな変換を考える
oneshot shift/resetok, but
partially okprompt-less s/roneshot
Algebraic
Effects
研究紹介. 課題、今後の予定

asymmetriccoroutine
12/13

Dive into Algebraic Effects

自己紹介

Algebraic Effects
effect の型
デモポイント
AE Implimentations

Multicore OCaml
研究紹介
oneshot AE →oneshot s/roneshot s/r → AC
課題、今後の予定まとめ まとめ
Algebraic Effects が楽しいICFP 2018 や ML Workshop2018 にもAE 関連のトピック *5*6
Algebraic Effects 使おう
インプリいろいろなければ自作も可

研究やってます*5https://icfp18.sigplan.org/event/mlfamilyworkshop-2018-papers-programming-with-abstract-algebraic-effects*6

https://icfp18.sigplan.org/event/icfp-2018-papers-versatile-event-correlation-with-algebraic-effects

まとめ13/13

おわり 参考文献[BP15]

Andrej Bauer and Matija Pretnar.
Programming with algebraic effects andhandlers. In: Journal of Logical and Algebraic
Methods in Programming 84.1 (2015),
pp. 108–123.

[KS16]

Oleg Kiselyov and KC Sivaramakrishnan.
Eff directly in OCaml. In: ML Workshop.
2016.

[Usu17] Chiharu Usui. One-shot Delimited
Continuations as Coroutines. MA thesis.
University of Tsukuba, 2017.