module type Empty = sig end
module TT (S : Empty) = struct
type t = T
end
module Mapper (S1 : Empty) (S2 : Empty) = struct
module C1 = TT (S1)
module C2 = TT (S2)
let map : C1.t -> C2.t = fun T -> T
end
module Make : functor (I : Empty) -> sig
type t = TT(I).t
end =
functor
(I : Empty)
->
struct
type t = TT(I).t
end
module type TT2 = sig
module I1 : Empty
module I2 : Empty
module T1 : module type of Make (I1)
module T2 : module type of Make (I2)
end
module Map (R : TT2) = struct
module I1 = R.I1
module I2 = R.I2
module M = Mapper (I1) (I2)
let map : R.T1.t -> R.T2.t = M.map
end
It says
The value M.map has type M.C1.t -> M.C2.t
but an expression was expected of type R.T1.t -> R.T2.t
Type M.C1.t is not compatible with type R.T1.t
However, changing the definition of the module Map to
module Map (R : TT2) = struct
module M = Mapper (R.I1) (R.I2)
let map : R.T1.t -> R.T2.t = M.map
end
makes the error go away. I am struggling to reconcile this with anything in my mental model of how modules work. I always thought that a statement like module I1 = R.I1 was just an alias or abbreviation, not anything generative. Is this a bug? Or am I misunderstanding something?
This is not a bug. It is a limitation of the current module system of OCaml that module aliases are not preserved through functor calls. This is one of the issues that “transparent ascription” would solve.
No, applying functor to two equal modules will always produce the same result (at the type level, runtime values are not shared between two different applications).
However, functors only have partial view of their argument and thus cannot alias them. In other words in
since Map is only seeing a slice of the module R, the module I1 cannot be an alias and have type R.I1 .
A first step towards transparent ascription will be to make alias more explicit, there is ongoing work to do so, and it might be reviewed in time for 5.5 .
Module aliases appearing in functor bodies making reference to functor parameters are “expanded”: for example, you can check in the toplevel that the functor F in
module type S = sig type t end
module F(X : S) = struct module Y = X end
has type
(X : S) -> sig module Y : sig type t = X.t end end
and not
(X : S) -> sig module Y = X end
This latter type would not be compatible with the compilation scheme of OCaml (or ML in general) in which structure components are accessed via statically known offsets since (X : S) may reorder or restrict the components of X to an arbitrary subset.
In your example, aliases I1 and I2 in the body of Map are similarly expanded, as if you had typed:
module Map (R : TT2) = struct
module I1 = sig end
module I2 = sig end
module M = Mapper (I1) (I2)
let map : R.T1.t -> R.T2.t = M.map
end
This breaks the connection of I1 and I2 with R.I1 and R.I2 so that Mapper (I1) (I2) is no longer compatible with Mapper (R.I1) (R.I2).
Okay, I think I get it. But that seems to me like extremely confusing notation then. Outside of a functor, or inside of a functor when the alias definition doesn’t refer to a functor parameter, the equals sign really does mean equals (right?). Since this sort of “alias” is actually doing something very different, it seems to me like it would have been better to use a different notation for it.
The equal sign always mean (structurally) equal. However, like for values there are two different type of equality for modules at play:
structural equality means that the contents of two modules is the same at type level,
for instance in
module M = F(Int)
module N = F(Int)
the two modules are structurally equal and for any type t in M, we have M.t = N.t = F(Int).t (for structural equality other component). This is the default equality, that is always true when you write module M = ....
identity equality means that two module paths are different aliases to the same object,
for instance
module A = Int
module B = Int
Let’s note this equality A == B. Currently, module definitions are implicitly promoted to alias definitions, when the programmer write module X = Path.To.Y inside a module or a submodule. In other words, the above would be equivalent to write in fantasy syntax
module A == Int
module B == Int
The reason that module aliases (the definitions of module with ==, see the “Type-level module aliases” section in the manual) were not made explicit when they were introduced is that most of the time structural equality is all that matters, and identity equality implies structural equality.
There is however a major case where identity equality matters: functor application.
Applying a functor only preserves identity equality: if A == B, then F(A) == F(B).
Contrarily, applying a functor to two modules that are structurally equal but not identity equal yields two modules that are not even structurally equal.
This means that before introducing module aliases, two functor application only yielded equal modules if the functor applications were syntactically equal, in other words in
module A = Int
module X = F(Int)
module Y = F(Int)
module Z = F(A)
only X and Y were considered equal. Module aliases lift partially this restriction.
The work on transparent ascription is based on the idea that it would be better to lift this restriction as much as possible while keeping applicative functor equality (and making the two kinds of slightly different equality more explicit when the difference matters).
I do really wish that identity equality was written with a different symbol like your fictitious ==. If I understand correctly, what’s going on in my case is that a module alias definition module A = Intusually actually means module A == Int, but if in place of Int I write some module path like R.M that involves a functor argument R, then the same syntax is silently reinterpreted to mean module A = R.M instead. I find that very confusing.