『Algebraic effects for Functional Programming』
Kokaを使ったAlgebraic Effectsの例や、Effects Typesの型推論やコンパイルに関する紹介
大まかな流れ
Abstract
Kokaを使った実際のAlgebraic Effectsの例を見ていく
例外処理、状態、イテレータ、async/awaitなど
1 Introduction
概要
2. Overview
Kokaを使った実際のAlgebraic Effectsの例を見ていく
例外処理、状態、イテレータ、async/awaitなど
型の表記法はτ → ε τ'
Kokaでは、effect typesは関数型にのみ発生する
つまり、通常の値(e.g. int)などには出現しない
effect typesを追跡するのにはcopeds labelsを持つRow Typesを使っている 例外の例
流石にsyntaxが今(v2.4.0)とぜんぜん違うmrsekut.icon
でもこれはこれで読みやすそう
code:koka(hs)
val to-maybe = handler {
return x -> Just(x)
raise(s) -> Nothing
}
polymorphismの話などKoka入門の内容を紹介しつつ、という感じ
handleはhandlerのsyntax sugger
m aからaを取り出すことを「discarge」と呼んでる
monadならrunHogeだし、algebraic effectsならhandlerを書くだけ
状態の例
resumeを説明しつつ
Iteratorの例
複数回resumeを使う例
他の言語ではあまり見られない
call/ccを持つ言語でのみ見られる
このへんまでは、知っとるな〜、という内容mrsekut.icon
全部docsに動くコードで書いてて、それを先に読んでた
Asyncの例
2.6. Domain Specific Effects: Parsing
これ以降読んでない
3. Type Rules
Kokaの型推論について
健全で完全
row-types based on scoped labelsらしい
4. Operational Semantics
5. Compilation
適切に型付されたプログラムが失敗しないことを証明する
一般的なランタイム言語(e.g. JS)へのAlgebraic Effectsの効率的なコンパイルについての説明