プログラム内のComputational Effectを形式的に記述する手法

Computational Effectをコンパイル時に静的に検証できる

型を拡張したEffect Componentで表現する

表示的意味論では 型 ! effects という表記がされる

読んでないが『Type and Effect Systems』でも ! が出てくるのがわかる

参考

とは #??

以下はUS wikiを読んだ理解なのでまったくふわっとしている

effect kindとregionを持つ

effect kind

region

リージョンのこと #??

Effect Systemで扱えるものの例

メモリの読み書き

線形型っぽい

ファイルのopen, close

継続、goto, COMEFROM文

JavaのChecked Exception

関連

Computational Effectを代数的に扱う

Effect Systemとだいたい同じ。

↑のことをAlgebraic Effectsと呼ぶ人もいるらしい ref

副作用

例

F*とか？

Haskell

↑この辺は、Monadしか扱えないHaskellの世界で、Monadの一般化であるEffect systemを表現しようとしたもの ref

OCamlのocaml-effects

Nim

参考

この論文が良いらしい

JS

haskell