Hi,
Peng Zang < peng.zang%40gmail.com">peng.zang
gmail.com> writes:
> - ---------
> module F = struct
> type t = { a : int; b : int; }
> let fooval = { a = 1; b = 2 }
> end;;
> module F1 = F;;
> module F2 = F;;
>
> F1.fooval;;
> F2.fooval;;
> [F1.fooval; F2.fooval];;
>
> (*** yields: ***)
>; - - : F1.t = {F1.a = 1; F1.b = 2}
> - - : F2.t = {F2.a = 1; F2.b = 2}
> - - : F1.t list = [{F1.a = 1; F1.b = 2}; {F1.a = 1; F1.b = 2}]
> - ---------
>
> In the second test, I make F into a functor (which actually doesn't
> even use the module passed in, but whatever) and it breaks... due to the
> nominal type being "defined" at functor application time??
>
> - --------
> module type S = sig type t end
> module F (A : S) = struct
> type t = { a : int; b : int; }
> let fooval = { a = 1; b = 2 }
> end;;
> module F1 = F (struct type t = int end);;
> module F2 = F (struct type t = int end);;
>
> F1.fooval;;
> F2.fooval;;
> [F1.fooval; F2.fooval];;
>
> (*** yields ***)
>; - - : F1.t = {F1.a = 1; F1.b = 2}
> - - : F2.t = {F2.a = 1; F2.b = 2}
> This expression has type F2.t but is here used with type F1.t
>; - --------
Questions about OCaml's module system and types are sometimes confusing, and
I'm actually not the right person for your question. But anyway, I can try to
make some points.
First, the compiler believes two types can be compatible because
- either they are structurally equivalent, e.g. (int * string) defined (and
exposed) in any module are considered equivalent
- or for nominally ones (record, variants, abstract type), there are type
equations defined on them
For an example,
<code>
module A = struct type t = {a: int} let x = {a = 1} end
module B = struct type t = {a: int} let x = {a = 2} end
module C = A
</code>
You'll see A.x and B.x are type incompatible due to the nominal type reason I
stated in previous mail, but A.x and C.x are compatible (note that their field
names are also different: C.a and A.a)
<;code>
# C.x;;
- : C.t = {C.a = 1}
# A.x;;
- : A.t = {A.a = 1}
# [A.x; C.x];;
- : C.t list = [{C.a = 1}; {C.a = 1}]
</code>
This is because when making module alias, the compiler add a type equation
automatically, as
<code>
# #tell "C.t";;
type C.t = A.t = { a : int; } (* note the "= A.t" part *)
</code>
Without it, module C behaves the same as B, even as an alias
<code>
# module type A = sig type t = {a: int} val x: t end;;
# module C : A = A;;
# [A.x; C.x];;
Characters 6-9:
[A.x; C.x];;
^^^
This expression has type C.t but is here used with type A.t
# #tell "C.t";;
type C.t = { a : int; } (* the equation is gone *)
</code>
Your first example corresponds to A.t ~ C.t test here, but note that alias is
not the root reason, type equation is. You second example, though it's a
functor application, but has the same effect as the plain A.t ~ B.t test here.
Because its result type F.t is actually defined from scratch, and has nothing
to do with the argument modules.
<code>
# #tell "F1.t";;
type F1.t = { a : int; b : int; } (* No type equation added here *)
# #tell "F2.t";;
type F2.t = { a : int; b : int; } (* No type equation here either *)
</code>
This, again, demonstrated that records are nominally typed.
More interesting is your example in previous email. Let's see what happened
actually:
<code>
# module A = Bar (Foo);;
# module B = Bar (Foo);;
# A.barprint B.barval;;
hi, 2- : unit = ()
# #tell "A.t";;
type A.t = Bar(Foo).t = { randstring : string; thefooval : Foo.t; }
# #tell "B.t";;
type B.t = Bar(Foo).t = { randstring : string; thefooval : Foo.t; }
</code>
Look, A.t = Bar(Foo).t and B.t = Bar(Foo).t, that's why they are
compatible. Without it, even though A.t and B.t have the same field names *and*
they are augmented by the same module Foo, nothing would save the compatibility.
<code>
# module type BAR = sig
type t = { randstring : string; thefooval: Foo.t }
val barprint: t -> unit
val barval: t
end;;
# module A : BAR = Bar(Foo);;
# module B : BAR = Bar(Foo);;
# A.barprint B.barval;;
Characters 11-19:
A.barprint B.barval;;
^^^^^^^^
This expression has type B.t but is here used with type A.t
</code>
Then, the renaming case
<;code>
# module X = Bar(Foo1);;
# module Y = Bar(Foo2);;
# #tell "X.t";;
type X.t = Bar(Foo1).t = { randstring : string; thefooval : Foo1.t; }
# #tell "Y.t";;
type Y.t = Bar(Foo2).t = { randstring : string; thefooval : Foo2.t; }
</code>
Look, A.t = Bar(Foo1).t and B.t = Bar(Foo2).t, the type equations don't
agree, just as Map.Make(Int32).t and Map.Make(Int64).t shouldn't equal.
Well, one may argue that FooX.t are concrete, and it's not dangerous to
consider all Bar(FooX).t equivalent. I agree this is subtle: in the first
example of this post, A.t and B.t are defined independently but with the same
representation and field names, still, A.x and B.x are not considered
compatible. The same reason applies here, Bar.(Foo1) is nominally different
from Bar.(Foo2), it doesn't matter whether their type "t" inside are actually
compatible or not. IMHO, modules are always treated nominally in OCaml, which
in turn serves as the foundations of all nominal typing.
Anyway, it won't be difficult to hint the compiler that Bar(Foo1) should equal
to Bar(Foo2). E.g.,
<code>
type ut = { randstring : string; thefooval : Foo.t };;
module Bar (Foo : FOO) = struct
type t = ut = { randstring : string; thefooval : Foo.t; }
let barprint t = Format.printf "%s, " t.randstring; Foo.fooprint t.thefooval
let barval = { randstring = "hi"; thefooval = Foo.fooval; }
end;;
</code>
HTH.
.
