Hatena::ブログ(Diary)

Oh, you `re no (fun _ → more) このページをアンテナに追加 RSSフィード

Ah well, a dromedary has one hump and a caml has reference cells, buffers, and a garbage collector.

2008-10-27

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 を思い出すのは私だけでは無いでしょう。Haskell の newtype の様な物、に見えなくも無いが、変換関数は自前で書かなきゃいけないし。ビミョーな代物だと言えましょう。

追記

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

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 の好きそうな手軽でオーバーヘッドのないハックではある。

osiireosiire 2008/10/28 04:49 PATはsubtype化だけは可能な少し緩い隠蔽な訳ですか。おっしゃる通り、使いどころが難しいですねぇ。勉強になります。

camlspottercamlspotter 2008/10/29 09:11 いやー、もしかしたら、もっとすごい役に立つ物なのかもしれんです。

スパム対策のためのダミーです。もし見えても何も入力しないでください
ゲスト


画像認証

トラックバック - http://d.hatena.ne.jp/camlspotter/20081027/1225076108