依存型とエフェクト

依存型とは、数字や文字列といった項に言及できる型のことを指します。このような型を用いると、プログラムの仕様を正確に表現することが可能になります。しかし、依存型付き言語の多くは、例外処理や破壊的代入などのエフェクトを許しません。これは、依存型によって得られる信頼性を実世界のソフトウェアに取り入れる妨げとなります。

そこで、本プロジェクトでは、エフェクトをもつ依存型付き言語を設計します。これまでに、叢の博士課程の研究によって、プログラムの実行を制御するためのツール限定継続命令に対する依存型システムが与えられています。アイディアとしては、型の依存性を純粋な（エフェクトを含まない）項に限定することで、型システムの健全性を保証しています。

今後は、型システムを代数的エフェクトとハンドラで拡張し、それに基づいた言語を実装する予定です。