effect systemについて

Haskellはモナドを用いて純粋・非純粋を切り分けることができる言語で、computational effectを扱うために導入されたものだった。

かつては関数 A -> B で一緒くたにしていたcomputationは、 A -> T B と、文脈 T をもった関数として表現できるようになった。ところでこのようなcomputational effectとしてのモナドを言語機能に組み込むには2つの方法があって、

Meta Language方式 (Haskell)
Programming Language方式 (MLなど)

(ここでは便宜上MetaLanguageとProgrammingLanguageと呼んでいて混乱しやすい名前なことは重々承知しているのだけれど他になんと呼べばいいのかわからないのでとりあえずこうしておく。MLはProgrammingLanguage方式なので注意)

前者はそのままモナドを言語の中に組み込む方法で、Haskellのようにユーザーがモナドを直接操作することになる。一方後者はKleisli categoryで考えましょうという方式で、言語に対して1つの巨大な(IO)モナド T を固定しておいて、 A -> B とプログラム言語の中でかいたら A -> T B だと解釈されるというもの。

さて、Haskellはモナドを直接ユーザーに見せることで、複数のモナドを切り替えてプログラムがかけるようにしたのだけれど、このせいで通常の関数とモナド付きの関数では互換性がなくなってしまった。

例えば 1 + 2 はよいけれど、 return 1 + return 2 は許されない。

さて、effect systemはいわば添字付きのモナドであり、プログラム A -> B を文脈 T とそこでのエフェクト e があって A -> Te B として表現するものである。effect systemも上に述べたようにそのモナドをユーザーに見せるかどうかを区別することが出来る。

表にまとめてみよう:

-	Programming Language	Meta Language
ベースの言語	`A -> B`	`A -> B`
monad system	`A -> B`	`A -> T B` …(2)
effect system	`A -> {e}B` …(3)	`A -> Te B` …(4)

effect systemを使うと同じモナドに対してどういう操作が起こる可能性があるかを調べることができる。詳しい話は省くけれど(2)から(3)に移ることは自然に出来て、effect systemは詳細に「起こりうる副作用」を分類することができる。

さて、(3)はProgramming Language方式なので実際にユーザーがモナドを意識する必要はないし、なによりpure functionとの互換性があるのが嬉しい。a : {e}Int と b : {e'}Int にたいして自然に a+b : {e | e'}Int などとできる。(これは厳密にはeffectの扱い方による)

おそらくHaskellよりももっと自然に副作用の分離ができるようになるはず。

ところで、(4)の用にエフェクトもモナドも記述するという方法があって、果たしてこれがどういうパラダイムになり、何ができるようになるのかは今の自分にはあまり想像できない。(便利なことがあるのだろうか？)

実装について

いくつか実装はあるけれど、例えばHaskellによく似たsyntaxを採用している Frank というのがある。この言語では A -> [e]B とかくと自然に forall eff. A -> {eff + e}B と解釈されてpolymorphic effectの計算が行われる。

少なくともよくあるeffect systemの定義ではcoerce rule(e < e' ~> {e}A -> {e'}A みたいなやつ)を入れずにこれを自然に計算する仕組みを考えてあって、個人的にはcoerce ruleをユーザーが手動で挿入するのはアホらしいのでこれがいいと思う。なので、そういうことをしようとすると既存のHaskellみたいな言語にそのまま組み込むわけには行かないので、個人的にはそろそろHaskell捨てたいな〜〜って言っている。

よい実装とライブラリがちゃんと揃ってくれないとどうしようもないのだけれど、いずれHaskellが捨てられる日がくるのだろうか。

はてさて