Phantom type ではちゃんと実装を隠蔽しましょう
コメント欄が無いのでトラックバックしておきます
http://d.hatena.ne.jp/tatta/20100623/
# isz (isz (lit 0)) - : bool term = IsZ (IsZ (Lit 3)) !!! isz : int term -> bool termなので型エラーになってほしいのに...
OCaml のバグじゃないかと疑っておられますが、バグではありません。Phantom type を使おうとされていますが、type 'a term = term_ の実装が見えていては幽霊の正体見たり枯れススキ。bool term = term_ = int term の関係が使えますから上の定義は問題ないのです。(ほんとうは問題があってほしい)
Phantom type を使うにはやはりその正体は隠しておかないといけません。OCaml では sig..end を使うか、別ファイルにして .mli を使うことで type 'a term = term_ の定義を隠蔽します:
module M : sig type 'a term 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_ val term_ : 'a term -> term_ val lit : int -> int term val inc : int term -> int term val isz : int term -> bool term val ift : bool term -> 'a term -> 'a term -> 'a term val pair : 'a term -> 'b term -> ('a * 'b) term val fst : ('a * 'b) term -> 'a term val snd : ('a * 'b) term -> 'b term end = struct 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 term_ x = x 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 end open M let _ = isz (isz (lit 0)) (* エラーになるョ *)
sig .. end の中で type 'a term = term_ という定義が無くなり、 'a term と term_ の関係が全く無くなっている事に注意してください。
term_ の定義を外に出すかどうかは、このモジュールをどう使うかによりますので、隠蔽してしまってもよかったかもしれません。'a term から term_ が欲しくなった時のために、term_ : 'a term -> term_ という関数を定義してみました。実際は恒等関数でしかありません。