学生のうちに知っておくべきOCamlのStructural Subtypingのこと

※コメント欄参照のこと

OCamlの型システムを見てると、Structural PolymorphismとStructural Subtypingという良く似た言葉が出てきます。この二つは一体なにが違うんでしょう。そもそも、OCamlってサブタイピングあったっけ?とか。そういう話。

OCamlで言うところのStructural Subtypingっていうのは、いわゆるSubtypingではありません。少なくとも教科書(TAPLとか)に載ってるSubtypingあり型システムよりも、かなり非力です。

偉大なるGarrigue先生のOCaml NG集に、Structural Subtypingの型付け規則が書いてある。これを見ると、関数型に関する規則が無いことがわかる。あんまりさらっと書いてあるので、一瞬、自明だから省略したのかと思いそうになるけど、そうじゃない。

試してみよう。

# ( Obj.magic 0 : < f: unit -> unit; g: unit -> unit > :> < f: unit -> unit > );;
- : < f : unit -> unit > = <obj>

これはOK。メソッドを減らす方向のcoercionは、スライドのWidthルールによりStructural Subtypingが成立する。それでは、関数型はどうなるか。普通の型システムだと、関数型のサブタイピング[tex:\tau_1 \rightarrow \tau_2 <: \tau_1' \rightarrow \tau_2']は、[tex:\tau_1 <: \tau_1' \wedge \tau_2' <: \tau_2]が成立するときに成り立つ。有名なcontravariantの話。つまり、< f: unit -> unit; g: unit -> unit > :> < f: unit -> unit >がOCamlでOKなことから(:>はOCamlのcoercion)、普通のサブタイピングならばこれを引数にした関数型同士のサブタイピングも成立しないとおかしい。

やってみる。

# ( Obj.magic 0 : < f: unit -> unit; g: unit -> unit > -> unit :> < f: unit -> unit > -> unit );;
Type < f : unit -> unit; g : unit -> unit > -> unit is not a subtype of type < f : unit -> unit > -> unit 

型エラー。

※ここだけ間違ってないと思う。

ちなみに、OCamlのマニュアルには「Subtyping is never implicit.」って書いてある*1。つまり、OCamlのプログラム中でStructural Subtypingが発動するのは、明示的にcoercionを書いたときだけ。例えば、< f: int -> float; .. >とか推論してくれるのでDuckTyping的でかっこいいぜーとかいう、それをStructural Subtypingと言うのは危ういと思う。

他の「Structural Subtyping」って言ってる言語(Scalaとか?)では、どういう意味なんだろう。Subtypingっぽいものを差してStructural Subtypingと言うのは、一般的なのでしょうか?

ただし、上に書いたような関数型は、普通にプログラムを書く限りでは列変数を含んだ型に推論されるので、「えっ、これサブタイピングじゃないのかよーー」みたいになることはあんまり無いと思います。あとObj.magic便利です＞＜

*1:どうでもいいけど、ずっとcoersionって書いてた件＞＜