Survey: A modular module system

module X = Y ではXという名前をもつモジュールにたいして、identifier Xiを 割り当てて、それをpath Yと定義する。等号の右に出て来るのがpathといった イメージ。pathはidentifierを情報として含んでいる。

(m) module expressionsはmodule X = ... の...に入る表現のこと。(X.Y.Z , struct .. endなど)
(s)はstruct ... endの間に入る定義たち
(M) module type はsig ... endかfunctor
(S) signaturesはsig ... endの中に入る個々の要素(C)の型

module type の strengthing M/p とはM の中に現われるabstruct typeの定義 type t::k を type t::k = p.t で置き換える操作。ただしtはtと同じ 名前を持ちidentifierはことなる。 tにたどり着くまでのパスを頭に付けるので(module Xi : M; S)/p = module Xi : M/p.X; S/p
M : sig type t end というsignatureのつくMに対して sig type t = M.t endという signatureはつかない。module M = ... (12)番からMの右辺の片付けのときには環境に Mという名前は入っていない。右辺には

• X.Y.Z 他のモジュールの参照
• struct .. end モジュール定義
• (m:M) モジュールに制限をかけたもの
• functor(X : M) m functor定義
• m(p) functor適用

がくるが、これらの中にはMは現われない。(名前の重複は許されていないので)
pathのstrengthingは module M = ... の右辺に現われるpathに対して 適用される。
例

module P = 
  (struct type t = int end : sig type t end) 

Pの右辺に対してpath Pでのstrengthingは起きない。

module M = P

Mの右辺にはpath Pが現われる。このPに対してpathのstrengthingを行う。

manifest型	type t = t'
opaque型(abstract型)	type t

(type t = t') : (type t = t'') [manifest-manifest] (1)
(type t = t') : (type t) [manifest-abstract] (2)
(type t) : (type t = t'') [abstract-manifest] (3)
(type t) : (type t) [abstract-abstract] (4)

用途
  (1),(4)はそのままか型のsubtypingによるマッチ
  (2)は実装の隠蔽
例
集合(Set)の利用
  集合自体は実装が見えなくて良い
  集合の要素の型は使用者が与えるが、これは集合演算で使われる型と、使用者が 与えた型とで互換性をもつ。 (集合にいれて出してつかおうとしたときに、元のかたと互換性がないとつかえないー)
Ocamlを元にして。Makeが集合を生成するfunctor

Make : (Ord : sig
               type t
               compare t -> t -> int
              end)
  sig
    type elt = Ord.t (* *)
    type t
    (* ..... *)
  end (* このsignatureはSにあたる *)

Makeの返すstructureの型はSとして名前を付けて定義されている。S内の要素型と引数の型に 互換性がなければならないので S with type elt = Ord.t という条件をつけている。
記述がすっきり+Sは名前がついているので他の所でも使える。

1.kindが異なる型のマッチ

# module BB = (struct type 'a t = 'a list end : sig type t end);;
               ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Signature mismatch:
Modules do not match:
  sig type 'a t = 'a list end
is not included in
  sig type t end
Type declarations do not match: type 'a t = 'a list is not included in type t

型変数が1と0のものはkindがマッチしないのでマッチしない

# module BB = (struct type 'a t = 'a list end : sig type 'b t end);;
module BB : sig type 'a t end

kindがマッチしている。

2.abstract(opaque)型の効用

# module IntSet = Set.Make((struct 
                                  type t = int
                                  let compare x y = if x > y then 1 else if x = y then 0 else -1 end
                                 : sig type t val compare: t -> t -> int end));;
module IntSet :
  sig
    type elt
    and t
    val empty : t
    val is_empty : t -> bool
    val mem : elt -> t -> bool
    val add : elt -> t -> t
    val singleton : elt -> t
    val remove : elt -> t -> t
    val union : t -> t -> t
    val inter : t -> t -> t
    val diff : t -> t -> t
    val compare : t -> t -> int
    val equal : t -> t -> bool
    val subset : t -> t -> bool
    val iter : (elt -> unit) -> t -> unit
    val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
    val for_all : (elt -> bool) -> t -> bool
    val exists : (elt -> bool) -> t -> bool
    val filter : (elt -> bool) -> t -> t
    val partition : (elt -> bool) -> t -> t * t
    val cardinal : t -> int
    val elements : t -> elt list
    val min_elt : t -> elt
    val max_elt : t -> elt
    val choose : t -> elt
  end
# let a = IntSet.add 1 IntSet.empty;;
Toplevel input:
# let a = IntSet.add 1 IntSet.empty;;
                     ^
This expression has type int but is here used with type IntSet.elt

Makeの引数のところでSetの要素型(Ord.t)を抽象型にしているので、intとしては使えない。

• Xavier Leroy: A modular module system