Just $ A sandbox

プログラミングと計算機科学とかわいさ

Notions of Computations and Effects

Haskell

前回のeffect systemに対するボヤキ、あるいは予言が色んな人に読まれたみたいなので興味がある人が一定数いるならeffect systemの紹介記事をちゃんと書こうと思った次第。

というわけでmonadを前提としてプログラミング言語的な見方と圏論的な見方を通してeffectに関するお話をしてみます。

注意 以下のプログラムはHaskellに寄せたオレオレsyntaxで実際にそういう実装があるわけじゃないので注意してください。実際の実装されている言語の話は最後に少しします。

programming with effects

effectは通常type-and-effect-systemと呼ばれるようにある意味で一種の型システムのようなものです。型システムがプログラムの入力と出力の値を見積もる仕組みだったのに対し、エフェクトシステムはプログラムを実行した際に「起きうる」エフェクトをコンパイラが見積もる仕組みだと思ってください。

で、これだけだと「つまりどういうこと？」ってなると思いますが、「エフェクトって何」って質問は「モナドって何」という質問と本質的に同じなので具体的には答えようがありません。というわけで例を見ましょう。

具体例

exception

-- exc effectの例
excHead :: List a -> {Exceptions [EmptyListError]} a
excHead [] = raise EmptyListError
excHead (x:xs) = x

これはエフェクトとして例外エフェクトを考えた場合です。{} の部分がエフェクトです。

ノリはEither monadやException monadと同じようなものでしょう。しかし、エフェクトは 暗黙的に計算されるので プログラム中で x と書いた部分は自然に {Exceptions} a 型の値になっています。

つまりエフェクトというのは自由に増やしてよく、subtypingのときのようにいつでも {es} a -> {es ++ es'} a のようなルール(coerce rule)が成り立ちます。

state

もう少し複雑な例をやりましょう。state effectは get, put というoperationを持っているエフェクトです。

-- get :: {State S} S
-- put :: S -> {State S} ()
addState :: Int -> {State Int} ()
addState n = put (get + n)

は〜めっちゃ簡単やんけ〜

io関連

Haskellではあらゆる「非純粋」をIOという謎の巨大モナドで隠蔽していましたが、エフェクトシステムではもう少し細かく制御することが可能です(もう少し細かく制御してもHaskellほどの煩わしさは出てきません)

readFileAndPrint :: FilePath -> {FileIO, Console} ()
readFileAndPrint path = print (readFile path) where
  print :: String -> {Console} ()
  readFile :: FilePath -> {FileIO} String

print . readFile としても型が合うことに注目してください。先程も言ったようにこれはエフェクトの暗黙的な計算によるものです。

effect handler

effectを発生させる関数はあちこちにあるので使いまくってるとどんどこ増えていくのでは、と思うかもしれませんが一般にeffectを減らすeffect handlerというものが存在します。(monadに対するrunMonadTみたいなやつ)

catExceptions :: List ({Exception} a) -> List a
catExceptions [] = []
catExceptions (x:xs) =
  handle x of
    value <a> -> a : catExceptions xs
    <raise -> k> -> catExceptions xs

syntaxは適当なのでノリで理解してもらうことにして、 {Exception} a 型の値が raise で作られたものか、あるいは普通の値なのかで場合分けが出来ます。そしてこのhandlerは必ずしも頭部だけではなく深部のoperationも同様にhandleできます。

divAllAndSum :: List Real -> Real -> Real
divAllAndSum xs t = calc where
  div :: Real -> Real -> {Exception DivideByZeroError} Real

  calc =
    -- map (\x -> x `div` t) xsの中で起きうるエラーをまとめてキャッチ
    handle (map (\x -> x `div` t) xs) of
      value <xs> -> sum xs
      <raise DivideByZeroError -> _> -> -1

で、まぁ「これってただの try..catch.. やんけ！」と思うと思いますがそのとおりで、effect handlerとは単なるtry-catchのeffectへの一般化です。

ちなみに説明してませんが本当はoperationをキャッチする時に k みたいな継続がやってきてこれを使って、operationが発生したときの途中のプログラムを受け取ってごにょごにょとかできるんですがまぁ今はスルーで

effect systemとは

さてeffect systemの例をいくつか見て雰囲気を味わったところでeffectの説明をしましょう。

さて「モナドって何」という質問には、(それが初学者に対する適切な説明かはともかく)「returnとbindがある型クラスです」という答えがあるのでそういう説明をすると、エフェクトとは次のような型クラスです。

class Effect e where
  return :: a -> {} a
  (>>=) :: {e} a -> (a -> {e'} b) -> {e ++ e'} b
  coerce :: e ⊆ e' => {e} a -> {e'} a

  -- もちろん満たすべき等式とかあるけど
  -- そのへんはあとで述べるよ

「モナドと一緒やんけ！」と思うと思いますがそもそもここでのeffectとはモナドをちょこっと拡張しただけのものなのでそりゃそうです。で、上に述べたeffect systemはこのeffectの計算(e ++ e' とか e ⊆ e' とか)を全てコンパイラがやってくれるので基本的にプログラマーは気にしなくて良いです。

やったぜ。

implicit vs explicit

さて上の定義は実は色んなことが隠蔽されており、そもそもコンパイラがやってくれるって何だよ、とかeffectに入ってる構造は何やねんみたいな話になります。で、上の方式は実はimplicit effect systemと呼ばれるもので、要はeffectの本当の姿は全て隠蔽して見せていました。

要はML等の言語では A -> B と書いたらこれはHaskellでいうところのIOモナドが隠蔽されており、実際には A -> IO B の意味である、とちょうど同じように、上ではエフェクトが属する本来のモナドが隠蔽されています。

というわけで、本当の定義としては、エフェクトシステムとはモナドに添字のついたモノであり、次のような型クラスを満たすものです。

class EffectedMonad T where
  return :: a -> T{} a
  (>>=) :: T{e} a -> (a -> T{e'} b) -> T{e ++ e'} b
  coerce :: e ⊆ e' => T{e} a -> T{e'} a

ここで T はモナドの一般化です。(e を固定するごとに T{e} がモナドになる、 わけではない ので注意)これを満たす T を適当に固定して、その T 部分を隠蔽すると上の例に出てくるような言語を定義することができるようになります。

graded monad

上に見たような EffectedMonad はモナドに見えるけど T{e} はモナドじゃない、と言いました。で当然このような構造にも名前がついており、 graded monad とか E-monad (Eはeffect category)とか言ったりします。

定義 graded monad T とは、preordered monoid E から [C,C] へのlax monoidal functorのことである。

monadとは 1 から [C,C] へのlax monoidal functorであったことを思い出せば自然にモナドの拡張になっています。

上でのcoerce ruleとは E のpreorderがmappingされたもの。

これで少しはスッキリ出来たんじゃないでしょうか。

実装の話

実装は次のようなものがあります。

後まぁまだまだあるはず。エフェクトの扱いが違ったりできることと出来ないことがあったりなかったりして割と言語ごとにノリが違うし、特にデファクトっぽい雰囲気のはないので興味ある人は色々やってみるといいんじゃないでしょうか。

Haskellにおける実装

せっかくHaskeller向けにあれこれ書いたのでHaskellの実装の話も。

この辺ちょい追記

さて上にも書いたとおりeffect systemはmonadの一般化なので、monadしか扱えないHaskellで完全な実装を書くのは不可能または激しく使いづらくなります。以下に述べる実装はそれを無理やりモナドに落としてそれっぽくしたのでまともなeffect systemだと思って(上に述べたような挙動を試そうとすると)GHCが文句を言ってきたり、普通のeffect systemならコンパイラがやってくれるエフェクトの計算とか推論を自力でやらされたりして大変です。

  • extensible-effects, freer-effects: 実はexteffはエフェクトシステムの部分的な実装と見ることが出来ます。freerはexteffの改良版でパフォーマンスもめっちゃ良くなってるので今ならこっちがおすすめ(freerよりfreer-effectsの方がいいらしい？)
  • extensible: extensible recordライブラリだったはずなんだけどいつの間にか同じノリでeffect systemの実装が生えていた。解説がこの辺とかにある
  • effect-monad: 上の EffectMonad (graded monad)を直接実装したライブラリ。どう見ても使いやすそうじゃない。

その他細々したこと

  • graded monadに興味ある人は論文を読んでくれ
  • 上では微妙に避けたけれどeffect handlerを定義するためにはeffect自体に制限的なものが必要になるのでそんなほいほい入れていいようなものでもないです
  • というか、割といくつかの言語では自分でeffectを新たに定義できるようになっていて、それがeffect handlerといい感じでアレがアレしてるんですが一言で言えるほど簡単な話じゃないと思う。
  • graded monadでじゃあ具体的にこういうeffect systemはどうやって考えるんですか、って思った人はやってみればいいんじゃないでしょうか。今なら論文になります。
  • というかeffect system関連今ならなんでも論文になるから論文書きたい人はやればいいんじゃないでしょうか。実装も意味論も未解決問題山積みですよ。

おわり