Just $ A sandbox

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

Notions of Computations and Effects

前回の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関連今ならなんでも論文になるから論文書きたい人はやればいいんじゃないでしょうか。実装も意味論も未解決問題山積みですよ。

おわり

monadからeffectへ

追記 もう少しまともなeffect入門記事を書きました

myuon-myon.hatenablog.com

この文章は今から5-10年後に万が一effect systemが流行り始め、今のHaskellのような立ち位置になった場合に備えて書いています。


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}Intb : {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が捨てられる日がくるのだろうか。

はてさて

ゲーム進捗報告会その4

進捗進捗ゥ!!!

進捗報告

ゲームシステム

  • スクリプトエンジン 簡単なスクリプトスクリプトエンジンを作った これでキャラクター画像の管理とかメッセージをリソースとして外部ファイルに丸投げできるようになったので良い感じ。演出とかで使っていく
  • エフェクター 画面上のWidgetと組み合わせてエフェクト(登場・消滅時にフェードさせたり)を管理するエフェクターというのを作った
  • フィールド 地図上で行きたいポイントを選ぶとそこへ行けるというタイプのフィールド機能を作ったりしていた(4/10)

ゲームの流れ

とりあえず本来の流れである、ゲームスタート→地図で場所を選ぶ→(例えば街なら)そこの各施設にアクセスして特定の操作ができるというのができるようになった。

あとは各機能を細かく作っていきたい。

設計

設計関連でも進捗があったのでまた別でまとめたい。とりあえず再帰でデータを管理する場合は注意が必要なことと、IORefは積極的に使っていけなどが知見です。

キャラデザとか

www.pixiv.net

NPCと街の雰囲気とかを少し絵に起こしたりしてた。キャラ絵は自分で描くとして、背景は自分ではかけないのでどうしようと思ってたけど、拙くても自分でなんとか頑張ってみようかなという気持ちが沸いてきた。ので背景絵も自分でなんとかするかも。

BGM等

そろそろBGM探すか…

TODO

現在のTODOは61/110でTODO消化率は55%です!進んでる!!

進捗報告とか体験版とか

まだまだ先の話だけど、進捗報告とか体験版配布する場所をブログ以外にちゃんと持っておきたいと思っていて、ファンティアとか無料プランも作れるからちょっと使ってみようかなと思っている。そこまで行けばだけど。