OCaml の type alias (type synonym) と non-parametric polymorphism
OCaml では普通のデータ型の定義 (type t = Foo | Bar や type t = { foo : int; bar : float }) とデータ型の別名宣言 (type alias もしくは type synonym: type int2 = int * int) の区別が希薄になっています。
もちろん内部では違いがごっちゃになっているというわけではなく、バグがあるというわけではありません。ただ、問題は、type alias が新しいデータ型を作ってしまうこと。例えば上述の int2 は、int * int という型と暗黙のうちに変換可能な新たなデータ型として定義されます。(より格好良く言うと、型 int2 と 型 int * int は 単一化可能(unifiable)。) *1
これと、ML のモジュールシステムの隠蔽を組み合わせると、型の意味がモジュールによって変わってしまう、という問題が起きます。ここで、型の意味は、まあ、漠然と、どの型とどの型が type alias されてるので、unifiable である、という意味だと思ってください。
m.mli
type int2 val x : int2 (* もはや int * int としては使えない *)
m.ml
type int2 = int * int let x = 1, 2 (* int * int にも int2 にも使える *)
例えば上のように signature (m.mli) で int2 の定義 int * int の alias、を隠蔽すると、モジュールM内部では int2 は int * int と unifiable であったはずなのに、Mの外では unifiable ではなくなります。
そんなの当たり前だって？確かにそのとおりで、この隠蔽機構があるあからこそ、 OCaml (より一般的に ML族)では実装の隠蔽やカプセル化が可能になって、生産性を上げることに成功しています。
しかし、この type alias の signature による隠蔽は、型依存の関数や値を考える時に困るのです。型依存の値っていうのは、ad-hoc polymorphism とか、non-parametric polymorphism とか、overloading とか、 generic とか言われているやつですで、polymorphic な値なんだけれど、instance された型によって全く異なる意味*2をとることができる値。例えば、こんなの:
# (zero : int) - : int = 0 # (zero : float) - : float = 0.0 # (zero : int list) - : int list = []
# add 1 2 - : int = 3 # add 1.2 3.4 - : float = 4.6
もちろん、OCamlではこんな値を作ることは不可能ですのでご安心ください。問題はわざわざコンパイラを改造してこんな値を作りたいと思っているヤツに発生するわけだ。
大雑把に言うと、究極的には、こういう non-parametric polymorphic な値は、式の instantiate された型をMLの値として得る関数 typeof が実装できれば、効率はともかく、実装することができる。
# typeof 1 - : type = <> (* < > ってのは型 t を表す値だと思ってくんねぇ *) # typeof 1.0 - : type = < >
この typeof とさっきの新しいデータ型を定義するOCamlの type alias と signature による実装隠蔽が相性悪いんだ。
- typeof x は <
> を返すべきなのか、それとも < > を返すべきなのか？ - m.ml 内部からの視点では、そもそも <
> っていう個別の値はありえるのか、alias なんだから、unifiable なわけで、< > = < > が成り立つのではないか？ - いやいや、m.ml外部からの視点では int2 は int * int と同じ型だ、というのは隠蔽されてしまうから、やはり、<
> <> < > でなければ困る。 - typeof x は m.ml 内では <
>、m.ml 外では < > ???
というわけで、モジュール文脈によって、type alias int2 の unifiability が変わってしまう OCaml において、 typeof 関数を定義できたとすると、その挙動も type unifiability の文脈依存性に引きずられて、モジュール文脈に依存してしまうわけ。*3基本の typeof にこういう問題があるので、non-parametric polymorphism な値すべてにこの問題は付きまとうことになる。これに関しては、
- キモイので却下。non-parametric polymorphism 必要なし。
- キモイけど、まあいいじゃん。 non-parametric polymorphism 便利だしさー。
- キモイから、なんとかしよう。
という三つの立ち位置があるわけだけど、GCamlは二番目の立場を取ってきた、というか、私がアホだったので、この問題を深く考えずに実装していたら二番目になっていた、というのが正しいな。これをなんとか三番目にしたいわけですね。
ちなみに、Haskell には type class っていう non-parametric なヤツがあるんだけれど、こんな問題はない。なぜなら、type synonym (alias) は隠蔽できないからだ。Int2*4はデータ型ではなくて type synonym なのであって、int2 という存在を知っているモジュールは、必ず、Int2 = (Int, Int) *5という aliasing も知っている。Int2 の aliasing の定義を隠蔽したい場合は newtype というものを使う。newtype Int2 = INT2 (Int, Int) と書くと、OCaml の int2 = int * int のような隠蔽できる alias のようなものが定義できるが、Int2 と (Int, Int) の型の間の行き来を明示的に INT2 というコンストラクタを使って書くことになる。
これと同じことを OCaml に導入すれば、当然だけど、今まで議論してきた問題は消失する。だけど、そんなことをすると、今まで書かれたほとんどすべての OCaml プログラムは修正なしには使えなくなる。なので、この方法は却下だ。何か良い方法があればよいのだが。
