#005 存在型(2)

先日 OCaml で存在型を実装する方法を紹介したが， 前回の例はあまり面白くないものだったので， こちらの記事にある存在型に対して同様の実装をしてみることにする． この記事にもあるように存在型は module として実装することも可能である （こちらの方が直観的でわかりやすい）． なお，この記事はクイズとなっているので，ついでにその解答にも簡単に触れる． たぶんこれで正解のはずだが，あのピッツ（仮名）が間違えたというのは少々驚いた． [06/09/01] 追記：実は解答の記事があったらしい．こっちのクイズ（？）はもっと難しそう．

クイズの内容や T, V1, V2 の定義についてはこちらを参照していただくとして， まず，この解答からはじめてみよう．結論から言えば，反例が存在するため文脈等価とは言えない． 例えば，ファンクタ F を

module F (T:T) = struct
  let rec q () = T.g (fun t -> let _ = T.g (fun _ -> t) && q () in t)
  let r = q ()
end

のように定義すると，module A1 = F(V1) は無限ループしてしまうが， module A2 = F(V2) は無限ループしない． && を || に変えればその逆になる．

さて，今度は以前紹介した多相型のフィールドをもつレコードの使う方法で実装してみよう． 存在型 ∃'a(('a->'a)->bool) は， ∀'b(∀'a((('a->'a)->bool)->'b)->'b) と等価なので次のように型を定義できる． 乱暴な言い方をすれば，後者は継続のようなものである．

type t = { f: 'b. 'b neg -> 'b }<br>
and 'b neg = { k: 'a. (('a->'a)->bool) -> 'b }

元の記事にある v1 と v2 は上の t 型をもつ値として，

let v1 = { f = fun k -> k.k (fun f -> f (); true) }
let v2 = { f = fun k -> k.k (fun f -> f true && not (f false)) }

と定義できる．一方，上記のファンクタ F に相当する関数も

let rec f v =
  v.f { k = fun g -> g (fun t -> let _ = v.f { k = fun _ -> g (fun _ -> t) } && f v in t) }

と定義することができる（もはや読むに耐えないが）． このとき，f v1 は無限ループするが，f v2 は無限ループしないことが確認できる． ここで，

let rec f v =
  v.f { k = fun g -> g (fun t -> let _ = v.f { k = fun g -> g (fun _ -> t) } && f v in t) }

としてはいけない．何も考えず前回のように書き換えると，ここで嵌ってしまう． このようなことを踏まえると前の記事で口走ったような camlp4 による自動化はかなり難しい気もしてきたなぁ． CPS 変換を利用すればうまくいくのだろうか？ if や && が非正格だったりして完全なものを作るのは非常に面倒な予感．