著者

川俣 楓河 寺内 多智弘

出版者

日本ソフトウェア科学会

雑誌

コンピュータ ソフトウェア (ISSN:02896540)

巻号頁・発行日

vol.40, no.2, pp.2_19-2_48, 2023-04-21 (Released:2023-06-21)

---

代数的エフェクトとハンドラとは,プログラム中のエフェクトの発生を抽象化してその動作をハンドラで定義するものであり,実装が分離されることでエフェクトを含むプログラムを見通し良く書くことができる.トレースエフェクトとは,プログラムの実行中に生じるイベントの発生順の列を静的に見積もったものであり,プログラムの時間的な性質の検証を可能にする.本論文では,代数的エフェクトハンドラとトレースエフェクトを共に備えることで,代数的エフェクトハンドラのエフェクト実装分離の利便性を享受しつつプログラムの時間的な性質を捉えることのできる型・エフェクトシステムを提案する.また,この体系の型安全性,すなわち正しく型付けされた項の評価は行き詰まらず,かつ型付けで得られたトレースエフェクトはその項の評価で発生し得るエフェクト列を保守的に見積もることを示し,さらにこの体系に対する健全性を満足する型推論を構築する.