Re: [Caml-list] module equality

[Jeremy Yallop <yallop@gmail.com>]

Dear Christophe,

On 20 June 2017 at 10:36, Christophe Raffalli <christophe@raffalli.eu> wrote:
> I thought that two applications of Set.Make to
> the same module would result in two distinct
> modules with two distinct types 't'.
>
> This is not the case

Right: in OCaml, two applications of a functor to the same module path
have signatures with equal type components.  This type of functor is
called "applicative", as opposed to the "generative" functors found in
Standard ML.  Generative functors have the behaviour you were
expecting, with each application generating fresh type components.
However, applicative functors allow many programs to be given types
that are rejected when functors are generative.  (There are a few
examples nowadays of programs that can be given types with generative,
but not applicative, functors, but they're fairly obscure.)

In your example:

> module F(O:Set.OrderedType) : S with type elt = O.t = struct
[...]
> module M1 = F(Int)
> module M2 = F(Int)

the two applications of F both have the signature

     sig ... type t = F(Int).t ... end

i.e. both M1.t and M2.t are equal to the type F(Int).t, and so values
of those types can be mixed freely.  However, although the types
resulting from the functor applications are shared, the values
resulting from the application (i.e. M1 and M2) are not equivalent.
People occasionally find this combination -- sharing of types without
sharing of values -- surprising, since types are often used to
determine whether values are compatible in terms of both
representation and behaviour.

There are a couple of ways to ensure that applications of F to the
same module build modules with incompatible types.  First, the
applicative behaviour only holds for paths, so you can force
incompatibility at the call site by passing a module expression that
is not a path as an argument:

   module M1 = F(struct include Int end)
   module M2 = F(struct include Int end)

  # fun (x : M1.t) -> (x : M2.t);;
  Characters 19-20:
    fun (x : M1.t) -> (x : M2.t);;
                       ^
  Error: This expression has type M1.t but an expression was expected of type
           M2.t

Alternatively, you can mark the functor as generative at the
definition site by adding an additional parameter '()':

   module F(O:Set.OrderedType) () : S with type elt = O.t = struct
   ...

which requires each caller of F to provide a corresponding argument

   module M1 = F(Int) ()
   module M2 = F(Int) ()

and once again generates modules whose signatures have distinct type components.

Since the surprising behaviour only arises when functor applications
have effects, Andreas Rossberg has advocated connecting the
applicative/generative distinction with the purity/effectful
distinction, making pure functors applicative and effectful functors
generative.  OCaml doesn't enforce this behaviour, but it's a
reasonably pattern to follow when writing programs.

Kind regards,

Jeremy