可変状態モナドと安全な入出力とセッション型 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

ここで、わかりにくいかもしれませんが は head(car)の要素の型が'a, tail(cdr)の要素の型が'bのheterogeneous list を表しています。 具体的には、例えば なら、 1番目の要素の型が closed 、 2番目の要素の型が input 、…などと読みます。

次に、何かしらの操作、例えば open_in の型を観てみます。ハンドル(チャネル)と、ファイルパスを与えると、ファイルが入力専用で開かれる、という操作です。

val open_in : ('a, closed -> input) handle -> string -> ('a, unit) monad
  • ('a,..) handle と ('a, ..) monad のように、 型が一致しているところがミソです。 monad の 状態遷移(?)は 'a の通りであるよ、というわけです。
  • 一方、 ch1 の型 ( -> , 'a -> 'c) handle と、open_in の引数の型 ('a, closed -> input) handle の 第一型引数 unify してみると、 -> となります。
  • は heterogeneous list だと書きました。結局 この open_in ch1 "..."という操作の型は ( -> , unit) monad となり、もしこれが状態モナドだったらば heterogeneous list の 0番目の要素の型を closed から input に書き換えている操作だ、と読めます。

結局

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...)

セッション型のdualとかをモジュールを使って表現してやる必要アリ。詳しくはTovのページのOCaml実装を参照。

(* an incomplete implementation of session types in OCaml. by Keigo IMAI (http://d.hatena.ne.jp/keigoi/ ) *)

type ('i,'j,'a) monad = Monad of ('i -> 'j * 'a)   (* variable-state (indexed) monad *)

(* standard operations on monads *)
let return : 'a -> ('b, 'b, 'a) monad = fun a -> Monad (fun b -> (b,a))
let bind : ('a, 'b, 'd) monad -> ('d -> ('b, 'c, 'e) monad) -> ('a, 'c, 'e) monad = 
      fun (Monad m1) f -> Monad (fun a -> match m1 a with (b, d) -> match f d with (Monad m2) -> m2 b)
let ( $ ) : ('a, 'b, unit) monad -> ('b, 'c, 'd) monad -> ('a, 'c, 'd) monad = 
      fun m n -> bind m (fun _ -> n)


type ('i,'j,'x,'y) index = Idx of ('i -> 'x * ('y -> 'j)) (* index which points to a `store' in a monad *)

(* there's a design decision on where to put real channels, 
   i.e. whether to store channel in the indices or not. 
   we do not store channels in the index, to prevent users from abusing it.
   Hence ('i,'j,'x,'y) index represents only an index (or type-level number), not a channel. *)

(* index to access to the stores *)
let id1 : (<c:'x;n:'b>, <c:'y;n:'b>, 'x, 'y) index = 
      Idx (fun i -> i#c, (fun y->object method c=y method n=i#n end))
let id2 : (<c:'a;n:<c:'x;n:'b> >, <c:'a;n:<c:'y;n:'b> >, 'x, 'y) index = 
      Idx (fun i -> i#n#c, (fun y->object method c=i#c method n=object method c=y method n=i#n#n end end))
(* ... arbitrary many numbers can possible  ... *)

type ended = <c:unit; n:ended> (* all stores are closed *)
let run : (ended, ended, 'a) monad -> 'a = let rec ended _ = object method c=() method n=ended () end in 
      fun (Monad f) -> match f (ended ()) with (_, a) -> a

(* states, or `stored operations' *)
type ('a, 's) send = Send of ('a -> 's) (* send a value of type 'a, then 's *)
type ('a, 's) recv = Recv of (unit -> 'a * 's)  (* receive a value of type 'a, then 's *)
type close = Close of (unit -> unit) (* close *)

(* operations on states *)
let open_idx : ('i,'j,unit,'x) index -> 'x -> ('i,'j,unit) monad = 
      fun (Idx f) x -> Monad (fun i -> match f i with (_, next) -> (next x, ()))
let send : ('i, 'j, ('v, 's) send, 's) index -> 'v -> ('i, 'j, unit) monad = 
      fun (Idx f) v -> Monad (fun i -> match f i with (Send out, next) -> (next (out v), ()))
let recv : ('i, 'j, ('v, 's) recv, 's) index -> ('i, 'j, 'v) monad = 
      fun (Idx f) -> Monad (fun i -> match f i with (Recv inp, next) -> let (v,s) = inp () in (next s, v))
let close : ('i, 'j, close, unit) index -> ('i, 'j, unit) monad = 
      fun (Idx f) -> Monad (fun i -> match f i with (Close f, next) -> f (); (next (), ()))


type chan = (in_channel * out_channel)
(* making session types. dualization is not supported. to make one, refer to
   http://www.ccs.neu.edu/home/tov/pubs/haskell-session-types/ *)
let mk_send : ('v -> string) -> (chan -> 's) -> chan -> ('v, 's) send = fun f s ch -> Send (fun v -> output_string (snd ch) (f v); s ch)
let mk_recv : (string -> 'v) -> (chan -> 's) -> chan -> ('v, 's) recv = fun f s ch -> Recv (fun _ -> (f (input_line (fst ch)), s ch))
let mk_close : chan -> close = fun ch -> Close (fun _ -> close_out_noerr (snd ch); close_in_noerr (fst ch))


(* example *)
(*
let usage = mk_send (string_of_int) (mk_recv (float_of_string) mk_close);;
let _ = open_idx id1 (usage (...open chan...)) $ send id1 1 $ bind (recv id1) (fun v -> close id1);;
*)