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の型クラスを使っても同じようなことができるかもしれない。
Flexハック
flexといっても，adobeのやつではなく，スキャナージェネレータの方．
以下のようにflexの-Sオプションでオリジナルのスケルトンファイルを指定することで，生成ファイルをいろいろと調整することができる．応用例としては，Linuxのkernel moduleに組み込むための字句解析器を生成させたり，等．
$ flex -S myflex.skl -o mylexer.c mylexer.l
#http://www.hatena.ne.jp/my 本来，スケルトンファイルはflexの開発者向けの機能らしいが．．．
スケルトンファイルは，基本的にflexのソースに含まれているflex.sklをベースに自分好みにカスタマイズすれば良いのだが，そのままでは使えない．flex.sklはm4マクロで前処理を行う必要があるのだ．
（flex-2.5.33の場合）以下のようにして，flex.sklを前処理する．
$ sed 's/m4_/m4postproc_/g; s/m4preproc_/m4_/g' flex.skl | m4 -P -DFLEX_MAJOR_VERSION=2 -DFLEX_MINOR_VERSION=5 -DFLEX_SUBMINOR_VERSION=33 | sed 's/m4postproc_/m4_/g' > myflex.skl
あとは，myflex.sklを好きなふうにいじればよい．
Hashtblにはまった
OCamlのHashtblは，(=)演算子による構造比較なのに気がつかなくて，はまってしまった．
# let key = ref 0;;
val key = int ref {contents = 0}
# Hashtbl.add tbl key ();;
- : unit = ()
# Hashtbl.mem tbl key;;
- : bool = true
# key := 1;; // <-- keyの中身を更新
- : unit = ()
# Hashtbl.mem tbl key;;
- : bool = false // <-- 値が取れなくなるここで，keyの値を0に戻すと，再び値が取れるようになる．．．
(==)で比較してほしかったなあとも思うが，そうするとstring型をキーとしてうまく使えなくなってしまうのか．
悩ましいところではある．
OCamlのバグ？
以下のようなヴァリアント型を定義する．
type term_ = | Lit of int | Inc of term_ | IsZ of term_ | If of term_ * term_ * term_ | Pair of term_ * term_ | Fst of term_ | Snd of term_ type 'a term = term_
そして，これらのコンストラクタ用の関数を以下のように定義する．
let lit n:int term = Lit n let inc (t:int term): int term = Inc t let isz (t:int term): bool term = IsZ t let ift (b:bool term) (t1:'a term) (t2:'a term) : 'a term = If(b,t1,t2) let pair (t1:'a term) (t2:'b term) : ('a * 'b) term = Pair(t1,t2) let fst (t:('a * 'b) term): 'a term = Fst t let snd (t:('a * 'b) term): 'b term = Snd t
上記のコンストラクタ関数を使ってみると．．．
# inc (lit 3) - : int term = Inc (Lit 3) # isz (lit 0) - : bool term = IsZ (Lit 0) ここまではOK # isz (isz (lit 0)) - : bool term = IsZ (IsZ (Lit 3)) !!! isz : int term -> bool termなので型エラーになってほしいのに．．．
type 'a term = term_
と定義しているので，その部分で型情報がうまく伝播してくれてないような気がする．仕様なのかバグなのか微妙なところだ．
OCaml: let recの多相
OCamlで，let recで定義した多相関数は，束縛の右辺では多相にならないことに気がついた．
let rec id x = x
and y () = id 0 and z () = id true;;
^^^^intでないのでエラーになる
OCaml: 型検査が通らない例
カリー化された関数opとそれに適用する引数をリストで受け取り1つずつ適用するようなexpand_args関数を以下のように定義する．
let rec expand_args op args = match args with
[] -> op
| v::rest -> expand_args (op v) rest以下のように使いたい．
# expand_args ( + ) [1;2];; > 3 # expand_args ( ^ ) ["foo";"bar"];; > "foobar"
残念ながら，expand_argsはOCamlの型検査をパスしない．opの型がexpand_argsの再帰呼び出しごとに異なってしまうからだ．'a, 'b->'a, 'b->'b->'a, 'b->'b->'b->'a, ...のように．
rectypesオプションを付ければ，expand_args関数自体は型検査をパスするようになるが．
# expand_args ( + ) [1;2];;
^^^^^
int->'a as 'aを期待しているが，int->int->intなので，型エラーとなるexpand_argsを所期の目的どおりに使えるようにするには，OCamlの多相型を拡張する必要がありそうだ．
OCamlの評価順序
# let x = ref 3 in (let () = x := 5 in !x) + !x;; - : int = 8 # let x = ref 3 in !x + (let () = x := 5 in !x);; - : int = 10
関数の引数の評価順序も同様
# let f x y = x + y;; val f : int -> int -> int # let x = ref 3 in f (x := 5; !x) !x;; - : int = 8 # let x = ref 3 in f !x (x := 5; !x);; - : int = 10
組型も同様
# let g (x,y) = x + y;; val g : int * int -> int # let x = ref 3 in g ((x := 5; !x), !x);; - : int = 8 # let x = ref 3 in g (!x, (x := 5; !x));; - : int = 10
ところが，letの評価順序は左から右だ！
# let x = ref 3 in let v1 = (x := 5; !x) and v2 = !x in v1 + v2;; - : int = 10 # let x = ref in let v1 = !x and v2 = (x := 5; !x) in v2 + v2;; - : int = 8
うーむ．
