Module definitions are not transparent?

The following code produces an error:

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.

See Section 2.4 of https://inria.hal.science/hal-04794404v1/file/3649818.pdf for an explanation.

Cheers,
Nicolas

Wow. That’s bizarre. So applying a functor to two equal modules won’t produce equal results.

Are there any prospects of having transparent ascription in the near future?

See Transparent ascription by clementblaudeau · Pull Request #54 · ocaml/RFCs · GitHub and the discussions linked therein.

Cheers,
Nicolas

1 Like

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

module Map (R : TT2) = struct
  ...
  module I1 = R.I1
...
end

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 .

4 Likes

Okay, so the equals sign in I1 = R.I1 doesn’t actually mean equals? What does it mean?

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).

Makes sense?

Cheers,
Nicolas

2 Likes

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.

Where is this documented in the manual?

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).

4 Likes

Thanks for that clear explanation!

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 = Int usually 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.