改造 GCaml の書き直しもしくは $Caml #3: $-abs unification を制御する

OCaml GCaml

さて、じゃあ今度は plus と minus を同時に使ってみましょう。
毎度あんまり面白くない例ですが、x + x - x を計算する(つもりの)関数 id を、前回の plus を参考に書いていみます:

let plus : $:(d : 'a -> 'a -> 'a) = d
let minus : $:(d : 'a -> 'a -> 'a) = d
let id x = minus (plus x x) x

さて、id は plus と minus を使っているから、(+) と (-) を渡して int に対して計算を行おうとすると、うまくいきません:

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

あれ？関数を渡すべき $-arg が一つしかありません。Unify されちゃった…:

let id $:d x = minus $:d (plus $:d x x) x

そう、型が同じだから $-abs unify されちゃったのです。これでは (+) と (-) を別々に渡したいのに、無理ですね。これを避けるには、plus と minus の $-arg が $-abs unification の対象にならないようにする必要があります。これを避けるには、二つの方法があります:

  • 各々の $-arg の型を違う物にする
  • $-label の名前を変えて、違った名前を持つようにする

$-arg の型を変える

うん、確かにお互いの引数の型を違う物に変えれば、$-abs unification は起こらない、でも両方とも 'a -> 'a -> 'a だからダメ？大丈夫です。別々のコンテナ型を作ってあげましょう:

module Plus : sig 
  type 'a t
  val plus : $:'a t -> 'a -> 'a -> 'a
end = struct
  type 'a t = 'a -> 'a -> 'a
  let plus $:(d : 'a t) = d
end

module Minus : sig 
  type 'a t
  val minus : $:'a t -> 'a -> 'a -> 'a
end = struct
  type 'a t = 'a -> 'a -> 'a
  let minus $:(d : 'a t) = d
end

ほら、こうすれば、'a Plus.t と 'a Minus.t は実は両方共 'a -> 'a -> 'a として定義されているんだけど、別の型になりました。Plus.t, Minus.t の実装を隠すのは、隠さないとお互いの定義が見えてしまって、型システムが 'a Plus.t と 'a Minus.t が同じだと判断してしまう(そしてやっぱり $-abs unification が起こってしまう)のを防ぐためです。
これ自体はよいのですが、$-arg の型の実装が隠蔽されてしまいました。そのまま、 Plus.plus $:(+) 1 2 と書いても 'a Plus.t と 'a -> 'a -> 'a が同じ事はモジュールの外では判らないのでエラーになります。なので、面倒なんですが、(+), (+.), (-), (-.) といった dispatch に使う値 (overloading instances) はモジュールの中に取り込んであげなくてはいけません:

module Plus : sig 
  type 'a t
  val plus : $:'a t -> 'a -> 'a -> 'a
  val int : int t
  val float : float t
end = struct
  type 'a t = 'a -> 'a -> 'a
  let plus $:(d : 'a t) = d
  let int = (+)
  let float = (+.)
end

module Minus : sig 
  type 'a t
  val minus : $:'a t -> 'a -> 'a -> 'a
  val int : int t
  val float : float t
end = struct
  type 'a t = 'a -> 'a -> 'a
  let minus $:(d : 'a t) = d
  let int = (-)
  let float = (-.)
end

こうすれば、

# let id x = Minus.minus (Plus.plus x x) x;;
val id : $:'a Minus.t -> $:'a Plus.t -> 'a -> 'a = <fun>
# id $:Minus.int $:Plus.int 3;;
- : int = 3

とうまく書いてやることが出来ます。

$-label の名前を変える

実は、$-arg unification が起こるのは、同じ型かどうかだけじゃなくて、ラベルも同じでなくてはいけない、という条件を入れています。だから、ラベルを変えるという方法でも、起こってほしくない unification を抑制することが出来ます:

let plus : $plus:(d : 'a -> 'a -> 'a) = d
let minus : $minus:(d : 'a -> 'a -> 'a) = d
let id x = minus (plus x x) x

とすると、

val id : $minus:('a -> 'a -> 'a) -> $plus:('a -> 'a -> 'a) -> 'a -> 'a =
  <fun>

なので、ちゃんと (-) と (+) を渡すことが出来ます。

# id $minus:(-) $plus:(+) 3;;
- : int = 3

この二つの方法のうちどっちが便利なのかはまだよくわかりません。後者の方が簡単そうに見えますが、自動的な overload resolution を考え出すと、モジュールという綺麗な枠を作って search space を制限できる前者の方が、限定していない後者より簡単に効率よく resolution 出来るのではないかと感じています。