I cannot wrap my head around equality of modules in OCaml. Functors are supposed to be applicative (that's what the Internet claims), but this seems to fail sometimes, and I cannot quite see the general rule behind it.
That's my example code:
module type PT = sig end
module P = struct end
let () =
Random.self_init ()
module OrigHashtbl = Hashtbl
module Hashtbl = struct
module Make(Hash: OrigHashtbl.HashedType) = struct
let random = Random.int 1000000
type 'a t = { t_list: (Hash.t * 'a) list }
let create _ =
Format.printf "Random %d@." random;
{ t_list = [] }
let mem ht v =
Format.printf "Random %d@." random;
List.mem_assoc v ht.t_list
end
end
module Hash = struct
type t = int
let equal x1 x2 = x1 = x2
let hash x = x
end
module Wrap(P: PT) = struct
module H = Hashtbl.Make(Hash)
end
module Wrap1 = Wrap(P)
module Wrap2 = Wrap(P)
module H1 = Wrap1.H
module H2 = Wrap2.H
let () =
let ht = H1.create 16 in
Format.printf "%b@." (H2.mem ht 0)
Code at ideone: https://ideone.com/5C8Muk
What I do here is I create a dummy implementation of some functions from Hashtbl
module and wrap it in the functor Wrap
which I 'call' twice, creating H1
and H2
which can be used interchangeably despite them being different modules that capture different value of random
:
$ ./test.byte
Random 501586
Random 681009
false
This is expected, because, as the Internet claims, OCaml functors are applicative.
But then I try to move the Hash
module inside Wrap
and the program stops compiling.
module Wrap(P: PT) = struct
module Hash = struct
type t = int
let equal x1 x2 = x1 = x2
let hash x = x
end
module H = Hashtbl.Make(Hash)
end
Code at Ideone: https://ideone.com/Gjxc32
$ ocamlbuild test.byte
+ /home/XXX/.opam/4.04.0/bin/ocamlc.opt -c -o test.cmo test.ml
File "test.ml", line 41, characters 35-37:
Error: This expression has type 'a H1.t = 'a Hashtbl.Make(Wrap1.Hash).t
but an expression was expected of type
'b H2.t = 'b Hashtbl.Make(Wrap2.Hash).t
Why is that? I'd expect that if Wrap1
and Wrap2
are the same module (because functors should be applicative, right?) then Wrap1.Hash
and Wrap2.Hash
are also the same. What's the general rule behind comparing modules?
Note: This is a continuation of another question How to convince ocaml that two functor instantiations are equal. There the only answer I got was along the lines of "OCaml functors are generative" which is false (at least sometimes).
Edit
Perhaps, I was wrong asking about module equality. What I'm actually interested in is type equality. Why in some cases Wrap1.H.t
equals Wrap2.H.t
and in some cases - not.
Answer
After a discussion with @Drup, things became more clear for me. Applicativeness means the following: if A = B
, then F(A) =/= F(B)
, but F(A).t = F(B).t
. For the modules defined inside F(A)
and F(B)
, things depend on how these modules are defined. In my example, whether or not Wrap1.H.t = Wrap2.H.t
depends on the definition of H
. In the variant that compiles, Wrap1.H.t = Hashtbl(Hash).t = Wrap2.H.t
. In the variant that does not compile, Wrap1.H.t = Hashtbl(Wrap1.Hash).t
and Wrap2.H.t = Hashtbl(Wrap2.Hash).t
, and they are distinct.
"Applicative functors" means that A = B
implies F(A).t = F(B).t
. It doesn't implies that F(A).M = F(B).M
. It's about types, not modules.
One fundamental difference between creation of types and creation of modules is that creating types is side-effect free (hence can be treated with an applicative behavior). Creating a module is not side effect free, hence you can't consider two different fresh modules as being the same. octachron gave a pretty good example in the last answer.
If you want to keep the equality while still having local modules, you can use module aliases. If you do this instead:
module Hash0 = struct
type t = int
let equal x1 x2 = x1 = x2
let hash x = x
end
module Wrap(P: PT) = struct
module Hash = Hash0 (* the type of this module is "= Hash0" *)
module H = Hashtbl.Make(Hash)
end
Then the program is accepted.
Note that, even in your failing version, Wrap1.Hash.t = Wrap2.Hash.t
holds (regardless of its definition), even if the modules are not equals.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With