Polymorphic Methodで遊ぶ

OCaml

自分用メモ。別に面白いことは書いてありません。

# class type c = object method id : 'a.'a -> 'a end;;
class type c = object method id : 'a -> 'a end

を考える。idの型に総称量化子がつかないのが気持ち悪い。

# let f x = begin x#id 1; x#id true end;;
This expression has type bool but is here used with type int

xの型は多相に推論されないのでダメ。

# let f (x:c) = begin x#id 1; x#id true end;;
Warning S: this expression should have type unit.
val f : c -> bool = <fun>

xの型をちゃんと宣言してやれば大丈夫。

さて、問題はここから。

# class b = object
    method f (x:int) = x
  end;;
class b : object method id : int -> int end

を考える。

# f (new b);;
This expression has type b but is here used with type c
Types for method id are incompatible

ふむ。まあ当然ダメ。これ、どうやってんのかちょっと気になる。推論されたわけではない型は、特殊な処理をしてるんだろうなあ。普通に単一化で取り扱おうとするとめんどくさそうかな。

ついでに。

# f (object method id x = x end);;
This expression has type < id : 'a -> 'a > but is here used with type c
The universal variable 'b would escape its scope

これもダメか。でもエラーメッセージが違う。どういう意味だろう。

# let id x = x;;
val id : 'a -> 'a = <fun>
# let a = object method id x = x end;;
val a : < id : 'a -> 'a > = <obj>
# id (a:>c);;
This expression cannot be coerced to type c = < id : 'a. 'a -> 'a >;
it has type < id : 'b -> 'b > but is here used with type #c
The universal variable 'c would escape its scope

むむ。さっきと同じエラーになった。つまりcoercionできなくてエラーになってるわけだな。しかしエラーの意味が謎。前半はいいとして、最後の「The universal variable 'c would escape its scope」が理解できん。'cってどこから出てきたんだろう。aの型くらいしか他には型変数が出てくるものはないけど…

わかったこと。

  • object式の型は一番外に∀がついた多相型
  • Polymorphic Methodの型検査は普通の多相型のとは違う

くらい。当たり前ですけど。