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_ という関数を定義してみました。実際は恒等関数でしかありません。