どうしてOCamlのオブジェクトにはcoersionが必要だったのか

let x = object
  method f x = x+1
  method g x = x-1
end;;

let y = object
  method f x = x*1
  method h x = x/2
end;;

List.map (fun x -> x#f 3) [x; y];;

上のようなプログラムは、絶対にエラーが発生しないにもかかわらず、肩推論で弾かれる。これを通るようにするには、明示的なcoersionを入れてやる必要がある。

List.map (fun x -> x#f 3) [(x :> < f : int -> int >); (y :> < f : int -> int >)];;

これって、めんどくさいような気がしていたのだ。[x; y]のようなリストに対して、< f : int -> int >のように共通部分のみを推論してやれれば、便利だと思う。この話は、一度JG先生に尋ねたことがあって、そのときは「型が読めなくなるから」と言う設計方針を聞いたことがあった。

その理由には、微妙になっとくできなかったんだけど、それがやっとわかった気がする、という話。

let z = object
  method f x = x+1
  method g x = x ^ ":";;

のようなオブジェクトがあったとき、明示的なcoersionを入れて< f : int -> int >へと変換する場合はなにも問題が生じない。しかし、このcoersionに相当する操作を自動でやろうとすると、[x; z]とかしたときに、メソッドgの型が一致しないことから、全体が型エラーになってしまうことになる。さらに、もっと悪いことに、x :: [y; z]ではエラーにならない(多分)。こっちだと、まず[y; z]が片付けされて、< f : int -> int > listになる。これにxを::しても、エラーにはならない。(一応soundにはなるけど。意味とかtyping ruleとか定義してないので直感的な意味で、ですが。)

ほとんど同じ意味のプログラムなのに、これでは混乱しそうだ。

ちなみにpolymorphic variantの場合は、こういう問題は生じない。objectのcoersionに相当する操作では、メソッドが減るobjectと逆にラベルが増える。

let f() = `A;;
let g() = `B;;
let list = [f(); g()];; (* ここで自動的にcoersionが発生する *)

こうすると型エラーになる。

let f b = if b then `A 1 else `B true;;
let g b = if b then `B "a" else `C (1.3);;
let list = [f(true); g(false)];;  (* これはエラー *)

この場合は、プログラムの意味的にもエラーとなるのが正しい。