2013-07-01 11 views
6

私はJavaのOOシステムの代わりにOCamlのモジュールシステムを使う方法についてのブログエントリを書いています(楽しい見通しです)。私は強要について理解していないことを見つけました。以下は基本モジュールとそれを含む2つのモジュールです:モジュールを含む、強制する

module M = struct 
    type t = int 
    let make() = 1 
end 
module A = struct 
    include M 
end 
module B = struct 
    include M 
end 

今、A.tとB.tは同じタイプです!どうして?それはあなたが

let a = A.make();; 
let b = B.make();; 
[a;b] --> A.t list (* ? *) 

をすれば、私はそれがプライベートタイプの略語で、これを防止することが可能です知っている、とあなたは同じリストに入れたいならば、強要使用evidientです。私の質問です:なぜこれは既に行われていないのですか? A.tB.tが同じ基本型から来ていることをコンパイラーはどのように知ることができますか?

よろしく
オルレ

答えて

8

これらの2つのモジュールに互換性があることを望むケースはたくさんあります。私は、コードの途中でExtHashtblの機能がHashtbl.tを使用することができ、または誰かによって構築されている値を操作するように、私は、ExtHashtbl.tHashtbl.tとの互換性を持つようにしたい

module Hashtbl = struct ... (* definition in the stdlib *) end 

module ExtHashtbl = struct ... (* my own layer on top of it *) end 

:シンプルなユースケースは以下の通りでありますそうでなければ、Hashtblライブラリについてのみ知り、自分のものは知りません。

MLモジュールの理論では、モジュール定義をできるだけ多くの方程式で強化し、署名にそれらを公開する「強化」という操作があります。その考え方は、より抽象度の高い(方程式の少ない)方が望ましい場合は、型シグニチャを使用して制約することができます。したがって、方程式を持つことは厳密に一般的です。

ファンクタの場合は状況が少し異なります。

module A (U : sig end) = struct include M end 
module B (U : sig end) = struct include M end 

MLのモジュールシステムでファンクタの二つの異なる概念、「生成的と呼ばれているものは、次にあります。代わりにシンプルなモジュールとしてAとBを定義するので、あなたがそれら空の署名のファンクタていたことを考えてみましょう(functorを呼び出すたびに、他の呼び出しと互換性のない "新鮮な"型が生成されます)、 "applicative"(同等の引数を持つfunctorのすべての呼び出しに互換性のある型があります) OCamlシステムは、名前のついたモジュール引数(より一般的にはパス)でインスタンシエートし、無名のモジュール引数でインスタンス化した場合、生成的な方法で動作します。

Xavier Leroyの2000年の論文A Modular Module System (PDF)(ウェブページA few papers on Camlから)で、OCamlモジュールシステムについて知りたいこと以上に多くのことを学ぶことができます。上で説明したすべての状況のコード例を以下に示します。

MLモジュールシステム、特にAnreas Rossberg、Derek DreyerおよびClaudio Russoによる最近の研究では、 "適用"と "生成"ファンクタの古典的な区別に異なった見方を持たせる傾向があります。 「純粋な」および「不純な」ファンクタに対応する必要があると主張しています。副作用を実行するファンクタは常に生成する必要がありますが、純粋な用語のみを使用するファンクタはデフォルトで適用する必要があります抽象化を提供する)。

module type S = sig 
    type t 
    val x : t 
end;; 

module M : S = struct 
    type t = int 
    let x = 1 
end;; 

(* definitions below are compatible, the test type-checks *) 
module A1 = M;; 
module B1 = M;; 
let _ = (A1.x = B1.x);; 

(* definitions below are each independently sealed with an abstract 
    signature, so incompatible; the test doesn't type-check *) 
module A2 : S = M;; 
module B2 : S = M;; 
let _ = (A2.x = B2.x);; 
(*This expression has type B2.t but an expression was expected of type A2.t*) 


(* note: if you don't seal Make with the S module type, all functor 
    applications will be transparently equal to M, and all examples below 
    then have compatible types. *) 
module Make (U : sig end) : S = M;; 

(* same functor applied to same argument: 
    compatible (applicative behavior) *) 
module U = struct end;; 
module A3 = Make(U);; 
module B3 = Make(U);; 
let _ = (A3.x = B3.x);; 

(* same functor applied to different argument: 
    incompatible (applicative behavior) *) 
module V = struct end;; 
module A4 = Make(U);; 
module B4 = Make(V);; 
let _ = (A4.x = B4.x);; 
(* This expression has type B4.t = Make(V).t 
    but an expression was expected of type A4.t = Make(U).t *) 

(* same functor applied to non-path (~unnamed) arguments: 
    incompatible (generative behavior) *) 
module A5 = Make(struct end);; 
module B5 = Make(struct end);; 
let _ = (A5.x = B5.x);; 
(* This expression has type B5.t but an expression was expected 
    of type A5.t *) 
4

私はまだ行っていないが、何を理解していない:あなたは、クラスを使用する場合は

+0

ありがとうございましたが、私の質問は哲学的なものでした。たぶんコンパイラが同じ型であると推測する理由は、可能な限りコンパイラが常に最も一般的な型を望んでいるからです。 –

関連する問題