Private abbreviation type

3.11 で導入された、Private abbreviation type を使って自然数を実装してみましょう:

module M : sig
  type nat = private int
  val nat_of_int : int -> nat
  val int_of_nat : nat -> int
end = struct
  type nat = int
  let nat_of_int n = 
    (assert (n >= 0));
    n
  let int_of_nat n = n
end

Mの外側では、 type nat = private int という情報があるので、コンパイラは nat という型を持つ値は int と同じく unboxed 31bit int (32bit アーキテクチャの場合) だとわかります。これは type nat = int と同じ。

普通の abbreviation type では、 type t = texp とすると、 t は texp の略称とみなされ、(signature でその事実が隠されない限り)同じ型として扱われます。実は、コンパイラ内では t と texp は別の型として扱われているのですが、単一化可能とすることで、同一視しています。

では t と texp の内部表現(実装)は同じだけれど、型上は別に扱ってほしい(つまり、単一化してほしくない)時はどうしたらよいのでしょう。

昔ながらの方法、 signature による実装の隠蔽:

module N : sig
  type nat
  val nat_of_int : int -> nat
  val int_of_nat : nat -> int
end = struct
  type nat = int
  let nat_of_int n = 
    (assert (n >= 0));
    n
  let int_of_nat n = n
end

M の外側では nat と int の関係は隠されているのでわかりません。なので、 nat と int の単一化もおこりません。nat_of_int, int_of_nat を通じてのみ、型の変換ができるようになっています。

じゃあ、これでいいじゃん。なんで、 private abbreviation type とか必要なの?

let m x = M.nat_of_int x = M.nat_of_int x
let n x = N.nat_of_int x = N.nat_of_int x

上の m と n は実は効率に違いがあります。m のほうが早い。M の外では M.nat は実装が int であることを知っているので、m では int 用の比較を使うことができます。n では N の外で N.nat がどういう実装の型かわかりませんので、より一般的な少し遅い比較関数を使うことになります。上のコードを全部つなげてひとつのファイル hoge.ml にして、

$ ocamlc -dlambda -c hoge.ml

とするとよくわかります:

     ...
     m/76
       (function x/77
         (== (apply (field 0 M/66) x/77) (apply (field 0 M/66) x/77)))
     n/78
       (function x/79
         (caml_equal (apply (field 0 N/75) x/79) (apply (field 0 N/75) x/79))))
    (makeblock 0 M/66 N/75 m/76 n/78)))

m では ==、 n では caml_equal を使っていますね。というわけで、unboxed なデータ型に関してしか意味がないようです。(boxed なら普通に signature 隠蔽でよい。) ocamlopt ではどうなるか知らないので誰か試してみてください。*1

しかしこの private abbreviation type、なんとなく型上の何かを制限すると言う意味で、 private type と似ていますが、実の所全然違うものです。片や型の単一化を(ほんとは同じ物なのに)制限、もう片方は値のコンストラクションの制限。予約キーワードは少ないほうがいいとはいえ、混乱の元ですね。C の static を思い出すのは私だけでは無いでしょう。Haskellnewtype の様な物、に見えなくも無いが、変換関数は自前で書かなきゃいけないし。ビミョーな代物だと言えましょう。

追記

ロクに調べないで書くとこういうことになるのですが、

let _ = fun (x : M.nat) -> (x :> int)

と書けます。逆は当然無理。private row っぽいね。もう訳わからんね。これが自動的だったら、private type と相性がいいのにね。

私の持論として、自分が理解していない/できない型システムを使っても良いプログラムは書けない。トラブルの元。よほどの事がない限り、使わないほうがよさそうです。そして、私は OCaml の subtyping は実の所理解できません。(というか理解しても惹玖様が変更しやがりなさるので追うのをあきらめた。)どうもありがとうございました。

  /\___/\
/ /    ヽ ::: \
| (●), 、(●)、 |                    Subtyping in OCaml! >
|  ,,ノ(、_, )ヽ、,,   |
|   ,;‐=‐ヽ   .:::::|
\  `ニニ´  .:::/      NO THANK YOU
/`ー‐--‐‐—´´\
       .n:n    nn
      nf|||    | | |^!n
      f|.| | ∩  ∩|..| |.|
      |: ::  ! }  {! ::: :|
      ヽ ,イ   ヽ  :イ   

*1:とか書いていると、コンパイラの頭さえよけりゃ、自動的にできる問題だから、そもそもこんなものいらないんじゃないかという気もしてきた。まあ、Pierre Weis の好きそうな手軽でオーバーヘッドのないハックではある。