可変状態モナドと安全な入出力とセッション型 in OCaml
今日は関数型言語の型で副作用(入出力)の制約を表現する、というお話を書きます。
(勢いで書いたので、わかりやすいかどうか不明です。)
Safeio in OCaml
ガリグ先生による Caml-list への投稿に Safeio というお話があります。
任意個のチャネルへの入出力に関して、
- 開かれたチャネルは必ず閉じられる
- 入力専用で開いたチャネルには入力しかできない
- 出力専用で開いたチャネルには出力しかできない
このような制限をOCamlの型で表現できるんですよ、というお話です。すごいですね。
Haskellで同じようなことをやっているネタとして、セッション型をHaskellで実装するお話があります。が、複数のチャネルを扱うために、どれも型クラスにヘビーに依存していたり(私やMatthew Sackmanの実装)、型クラスを使わない実装では複数のチャネルを管理するためにswapとかpopなどのアノテーションが必要(Pucella&Tovの実装)だったりします。
Haskellでやっている話がすべてそんな感じなので、そういう「型で遊ぶ」「型レベルリスト」みたいなお話はpure OCamlではやりにくいのかな、というのが私の感想だったのですが、、、実はMPTCもfundepsも要らなくてunificationだけでできるヨ、ということをガリグ先生の投稿は示しています。驚くべき発想です。
(polymorphic variant や object を使ってますが、必ず必要なわけでもないので、実のところHaskellでもできる?)
ですが、私の観測範囲でどこか論文なりWebサイトなりで言及されているのを見たことがありません（某社では実用されているとの噂も耳にしたのですが）
Indexed Monad, 可変(型)状態モナド, Shift/Reset in Haskell98 ...
話は変わりますが、Olegさんの記事にVariable (type)state `monad'というお話があります。
Haskell標準のStateモナド s -> (s, a) は状態の型が変えられないけれど、ここで「前の状態」と「後の状態」の型を変えて s1 -> (s2, a) のようにすれば計算の途中で状態の型が変わる、なんてことも表現できるわけです。
この場合、モナドの型は newtype State s1 s2 a = State (s1 -> (s2, a)) のような定義になります。
bind (>>=) の前後で型が整合しているという制限が加えられています。
一般に、こういうモナドは indexed monad と呼ばれ、他にも応用があったりします。
たとえば Delimited continuations with effect typing, full soundness, answer-type modification and polymorphism では、限定継続のShift/Resetの型付けにindexed monadが用いられています。正直私にはshiftやresetの型付けで何が起こっているのか未だにうまく理解できませんが、indexed monadのもうひとつの実用例です。 newtype C a b tau = C{unC:: (tau -> a) -> b} なので、継続モナドの一種であることはわかるのですが…
Safeio と indexed monad
実のところ、 上の記事のSafeio も indexed monad の一つです。 ('i -> 'j, 'a) monad というモナドのbindの定義は State s1 s2 a や C a b tau と同じように
val bind : ('a -> 'b, 'd) monad -> ('d -> ('b -> 'c, 'e) monad) -> ('a -> 'c, 'e) monad
と定義されています。→がいっぱいで読みにくいかもしれませんが…
('i -> 'j, 'a) monad は そのまま 「状態 'i から 状態 'j に遷移する操作」と読んで問題なさそうです。
Safeioにおける複数のチャネルの使われ方の追跡
しかし Safeio では ch1, ch2, ... と複数のチャネル(ハンドル)の使われ方を追跡できています。実のところ、Safeio の驚くべき点はそこにあります。
まずは チャネルの型を見てみます：
val ch1 : (<c:'a;n:'b> -> <c:'c;n:'b>, 'a -> 'c) handle
ここで、わかりにくいかもしれませんが
次に、何かしらの操作、例えば open_in の型を観てみます。ハンドル(チャネル)と、ファイルパスを与えると、ファイルが入力専用で開かれる、という操作です。
val open_in : ('a, closed -> input) handle -> string -> ('a, unit) monad
- ('a,..) handle と ('a, ..) monad のように、 型が一致しているところがミソです。 monad の 状態遷移(?)は 'a の通りであるよ、というわけです。
- 一方、 ch1 の型 (
結局
val ch1 : (<c:'a;n:'b> -> <c:'c;n:'b>, 'a -> 'c) handle val open_in : ('a, closed -> input) handle -> string -> ('a, unit) monad
という型で、 unification だけで heterogeneous list の特定の要素の書き換えを表現できているというわけです。
少なくとも私はビックリしました。
セッション型 in OCaml
上の技をより具体化して、 セッション型(の一部)を OCaml で実装しました。
http://ideone.com/umutf
- no channel passing
- no channel creation (but some kind of `session establishment' is available)
- no branch / choice (fatal...)
- no fork (thread creation) / parallelism (fatal...)
