GCamlで型レベル論理プログラミングっぽいこと

GCamlというOCamlにオーバーロード機能を追加した言語あるが、それの型推論機構をうまく使って、論理プログラミングっぽいことができないかと試行錯誤してみた。

まずは基本的な定数項を型として定義する。

type hanako = Hanako;;   
type taro   = Taro;;
type ichiro = Ichiro;;
type michio = Michio;;
type emiko  = Emiko;;
type soichi = Soichi;;
type haruo  = Haruo;;

次に、親子関係に関する事実parentをgenericな値として定義する。

let parent = generic (Hanako, Ichiro)   (* 花子の親は一郎 *)
                   | (Taro, Ichiro)     (* 太郎の親は一郎 *)
                   | (Ichiro, Michio)   (* 一郎の親は道夫 *)
                   | (Emiko, Michio)    (* 笑子の親は道夫 *)
                   | (Michio, Haruo)    (* 道夫の親は春雄 *)
                   | (Soichi, Haruo)    (* 宗一の親は春雄 *)
;;

parentに関する問い合わせは、以下のように関数を定義して使う。

let who_is_parent (x:'a) (y:'b) = ignore(parent:('a * 'b));;

実行例:

# who_is_parent Hanako;;
- : ichiro -> unit = <fun>      --- 花子の親は一郎です
# who_is_parent Ichiro;;
- : michio -> unit = <fun>      --- 一郎の親は道夫です

論理プログラミングっぽく逆方向の問い合わせもできる。。。

# (fun x y -> who_is_parent y x) Haruo;;
- : michio -> unit = <fun>

推論に失敗すると、型エラーとなる。

# who_is_parent Haruo;;
Type haruo -> 'a -> unit is not an instance of overloaded type
{ 'a * 'b < [| hanako * ichiro | taro * ichiro | ichiro * michio
             | emiko * michio | michio * haruo | soichi * haruo |] } =>
  'a -> 'b -> unit.

次に、祖父母関係を表す規則grand_parentをparentを使って定義してみる。

let grand_parent (x:'t) = fst (parent:('a * 't)), snd (parent:('t * 'b));;

ここで、余計に思える引数（x:'t）は実は重要で、これがないと、'tが単相型と判断されてしまうので、grand_parentが一回ぽっきりしか使えなくなってしまう。

そして、grand_parentに関する問い合わせは以下のように関数定義する。

let who_is_grandparent (x:'a) (y:'b) t = ignore((grand_parent t):('a * 'b));;

実行例はつぎのとおり。

# who_is_grandparent Taro;;
- : michio -> ichiro -> unit = <fun>   --- 太郎の祖父母は道夫
# who_is_grandparent Ichiro;;
- : haruo -> michio -> unit = <fun>    --- 一郎の祖父母は春雄
# (fun x y -> who_is_grandparent y x) Michio;;
- : hanako -> ichiro -> unit = <fun>   --- 道夫は花子の祖父母
# who_is_grandparent Michio;;  --- 失敗例
Type michio -> 'a -> 'b -> unit is not an instance of overloaded type
{ 'd -> 'e * 'f < { 'a * 'b < [| hanako * ichiro | taro * ichiro
                               | ichiro * michio | emiko * michio
                               | michio * haruo | soichi * haruo |],
                    'c * 'a < [| hanako * ichiro | taro * ichiro
                               | ichiro * michio | emiko * michio
                               | michio * haruo | soichi * haruo |] } =>
                    'a -> 'c * 'b } => 'e -> 'f -> 'd -> unit.
# (fun x y -> who_is_grandparent y x) Haruo;;
Type 'a -> haruo -> 'b -> unit is not an instance of overloaded type
{ 'd -> 'e * 'f < { 'a * 'b < [| hanako * ichiro | taro * ichiro
                               | ichiro * michio | emiko * michio
                               | michio * haruo | soichi * haruo |],
                    'c * 'a < [| hanako * ichiro | taro * ichiro
                               | ichiro * michio | emiko * michio
                               | michio * haruo | soichi * haruo |] } =>
                    'a -> 'c * 'b } => 'e -> 'f -> 'd -> unit.

最後の例（春雄は「誰」の祖父母？）が失敗しているのは、型推論のユニフィケーションにはバックトラックが無いからかと思われる。

Haskellの型クラスを使っても同じようなことができるかもしれない。