[Caml-list] module equality

[Caml-list] module equality

[Christophe Raffalli]

[-- Attachment #1: Type: text/plain, Size: 1457 bytes --]


Dear camelers,

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, and I am no sure it is a
good choice as it allows to write the following,
where you can break the invariant of a functor:

-------------------------------------------------------------------------
let is_prime n =
  let rec fn d =
      if d * d > n then true
          else if n mod d = 0 then false else fn (d+1)
	    in
	      fn 2

let rec random_prime n =
  let p = 2 + Random.int (n-2) in
    if is_prime p then p else random_prime n

module type S = sig
  type elt
  type t
  val create : elt list -> t
end

module F(O:Set.OrderedType) : S with type elt = O.t = struct
  type elt = O.t
  type t = O.t list
  let salt = random_prime 1_000_000
  let _ = Printf.printf "salf: %d\n%!" salt
  let f x = Hashtbl.hash (Hashtbl.hash x * salt)
  let cmp x y =
    match compare (f x) (f y) with
    | 0 -> compare x y
    | c -> c
  let create l = List.sort cmp l
end

module Int = struct
  type t = int
  let compare = compare
end

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

let _ = Printf.printf "test: %b\n%!" (M1.create [1;2;3;4;5] = M2.create [1;2;3;4;5])
----------------------------------------------------------------------------

OK, I know how to rewrite this functor so that M1.t and M2.t are distinct.
But still the above code should be rejected, shouldn't it ?

Cheers,
Christophe

[-- Attachment #2: signature.asc --]
[-- Type: application/pgp-signature, Size: 488 bytes --]

Re: [Caml-list] module equality

[Dario Teixeira]

Hi,

> 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, and I am no sure it is a
> good choice as it allows to write the following,
> where you can break the invariant of a functor:

OCaml functors have always been applicative.  However,
since 4.02 you can also declare generative functors,
which have the behaviour that you want:
http://caml.inria.fr/pub/docs/manual-ocaml/extn.html#sec253

Hope this helps. Cheers!
Dario Teixeira

Re: [Caml-list] module equality

[Jeremy Yallop]

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