Modal Effect Types
#論文
Wenhao Tang, Leo White, Stephen Dolan, Daniel Hillerström, Sam Lindley, Anton Lorenzen
（このページを書いた時点ではdraftで、arXivにあるのみ）
https://arxiv.org/abs/2407.11816
https://antonlorenzen.de/
Algebraic effects and handlersを扱う型システムの話。
以下のような状況を考える。
ターゲット言語は高階な関数型を扱える関数型言語にalgebraic effects and handlersが入ったもの。
Effect safeであり、かつ、accidental handlingが起こらないこと。
ハンドラの合成ができたり高階ハンドラが扱えたりすること。
更に、既存の言語に後からalgebraic effectsを入れる状況を念頭に、handlerを使っていない場面では元々の型を変えなくても型検査が通るようにしたい。
Kokaなどで採用されているrow-polymorphismベースのやり方だとeffect polymorphismを高階関数で使うために色々な場所でeffectが現れる。
nekketsuuu.icon ここ自分は実体験を伴っていないのでもうちょっとeffect handlersを使った実装をしてみないと本当には理解できなさそう。
そこで、関数ごとにその場で必要なhandlerを並べ上げるだけではなく、引き継がれてきた環境のeffect contextに比べて相対的にどのようなhandlerが必要なのかを注釈するスタイルを取り入れる。
つまりふたつのmodalityが登場する。
その場でeffect contextを上書きするabsolute modality [・]。論文の例だとgen: [yield](List Int -> 1)。
環境のeffect contextに加えたり消したりするrelative modality <・|・>。論文の例だとasList: <|yield>(1 -> 1) -> List Int
この方針で調べていくと、soundなeffect systemが考えられて、かつ色々必要そうな機能は持ち合わせている、というのが論文の内容。