改造 GCaml の書き直しもしくは $Caml #2: $-args を使って見る

えっとどこまで話したっけ?
ああ、$付きラベル引数($-arg)がどういう風にコンパイル(というか program transformation) されるかでした。省略可能引数と関数抽象で dispatch を実現しますと言うところまでだった。
じゃあ、実際にそれを使って見ましょう。
まず変な物を用意します:

# let plus $:d = d;;
val plus : $:'a -> 'a = <fun>

これは $ 付きの identity function。$一文字でも引数ラベルです。($hoge とかでもいいんですけど長いし、これからほとんどこの $ しか使いません。) この plus は GCaml では内部で invoker とか、個人的には the mother of all the overloaded values とか呼んでたものです。これが無いと始まらない。さて、

# plus $:(+) 1 2;;
- : int = 3
# plus $:(+.) 1.0 2.0;;
- : float = 3.

以上は普通ですね。$ の部分を普通のラベル付き引数にした時の挙動と同じです。これの何が面白いの?

面白いのは plus を使って double を定義するときです:

# let double x = plus x x;;
val double : $:('a -> 'a -> 'b) -> 'a -> 'b = <fun>

plus を字面上はあたかも普通の足し算のようにして double を定義しています。$-arg は省略されている。このコードは次のものと等価です:

let double $:d x = plus $:d x x

だから、

# double $:(+) 1;;
- : int = 2
# double $:(+.) 1.2;;
- : float = 2.4

になります。$-arg を持つ関数を、$-app を省略して使って別の polymorphic な値を定義してやると、自動的に対応する $-abs が導入されて、外側の $-arg がどんどん内側に受け渡されていくコードが簡単に作れるわけです。いちいち $:(+) とか、 $:(+.) って書くのが面倒くさいですが、それを書かずに済ますには他の改造が必要です。

auto $-abst unification

これも適当に作った用語です。$-抽象単一化?
上の plus と double で triple を作って見ましょう:

# let triple x = plus x (double x);;
val triple : $:('a -> 'b -> 'c) -> $:('a -> 'a -> 'b) -> 'a -> 'c = <fun>

あれ、$-arg が二つ、、、これはどう変換されるか考えればわかります:

let triple $:d1 $:d2 x = plus $:d1 x (double $:d2 x)

この triple で三倍を計算するには、triple $:(+) $:(+) 3 とか、 triple $:(+.) $:(+.) 1.2 とか書かにゃーいけません。ちょっと面倒ですね。うまく、一つの $-arg だけで済ます方法があります:

# let plus $:(d:'a -> 'a -> 'a) = d;;
val plus : $:('a -> 'a -> 'a) -> 'a -> 'a -> 'a = <fun>
# let double x = plus x x;;
val double : $:('a -> 'a -> 'a) -> 'a -> 'a = <fun>
# let triple x = plus x (double x);;
val triple : $:('a -> 'a -> 'a) -> 'a -> 'a = <fun>
# triple $:(+) 3, triple $:(+.) 1.2;;
- : int * float = 9, 3.6

前の例では plus の型は $:'a -> 'a だったのですが、足し算としては一般的過ぎる型なので、ここでは $:('a -> 'a -> 'a) -> 'a -> 'a -> 'a にしました。するとなんということでしょう! triple の $-arg の数が減ってしまいました! 変換はこうなっています:

let triple $:d x = plus $:d x (double $:d x)

triple が受け取った $-arg d が plus と double の両方に取り回されています。省略された、同じ型を持つ $-app は一つの $-abs に統一されます。これを個人的に auto $-abs unification って呼んでいます。


余談:
この「同じ型」というのは unification base の型システムではちょっと注意して扱わないといけない概念です。Free variable を持っていると今の瞬間は違う型でも後々の unification では同じ型になっちゃうかもしれない。例えば、let の型推論中に二つの $-arg の型が 'a -> 'a -> '_b と 'a -> 'a -> '_c という違った型があった時、auto $-abs unification は行われずにコンパイルを行って $:('a -> 'a -> '_b) -> $:('a -> 'a -> '_c) -> ... という型になりますが、その後の推論で、 '_b = '_c = int であることが判明しちゃった場合。結果は $:('a -> 'a -> int) -> $:('a -> 'a -> int) -> ... であって、$:('a -> 'a -> int) -> ... と一つには纏まりません。良く考えると GCaml にもあった問題です。

これから先のお話の流れ

  • plus と minus を同時に使う
  • 適切な overload instance を自動的に適用してホントの overloading を実現する