* Re: [Caml-list] types not equal when I expect them to be
2012-03-01 16:38 Ashish Agarwal
@ 2012-03-01 22:18 ` Gabriel Scherer
0 siblings, 0 replies; 3+ messages in thread
From: Gabriel Scherer @ 2012-03-01 22:18 UTC (permalink / raw)
To: Ashish Agarwal; +Cc: Caml List
Note that Bar is actually unnecessary. The following code exhibit the
exact same behavior:
module Foo = struct
module St = struct type t = string let compare = compare end
module Map (* : Map.S with type key = St.t *)
= Map.Make(St)
(* module Map = Map.Make(struct type t = string let compare =
compare end) *)
end
module Pack = struct
module Foo = Foo
end
let x : int Foo.Map.t = Pack.Foo.Map.empty
The important point is the interface of Map.Make when looked through
the environment (for example when rebound by `module F = Map.Make`,
then compiled with `ocamlc -i`):
functor (Ord : Map.OrderedType) ->
sig
type key = Ord.t
type 'a t = 'a Map.Make(Ord).t
...
end
Note the `'a t = 'a Map.Make(Ord).t` part: this is the result of
a so-called "strenghening" operation, where the abstract types `t` in
the signature of the module `M` are noted to be equal to `M.t`; this
allows `N` to remain type-compatible with `M` when writing `module N =
M`.
Now the result of this strenghtening operation in your case is that
your module Map defined in Foo has in its signature:
type 'a t = 'a Map.Make(Foo.St).t
The sorrow and non-intuitive point is that, after rebinding in Pack,
Pack.Foo gets the following signature:
type 'a t = 'a Map.Make(Pack.Foo.St).t
Those two type are not path-compatible because `Pack.Foo.St` is not
a path syntactically equal to `Foo.St` -- I'm not sure why the
type-checker couldn't check path equality upto known module aliasing,
however.
Now, why your fixes work:
1. by adding the `: Map.S with type key = ...` signature to your
Foo.Map module, you seal the module under the Map.S signature which
has its type `'a t` *abstract*. This cancels the effects of
strenghtening in the definition of `Foo.Map`. Now, in the
definition of Pack, aliasing `module Foo = Foo` re-apply
strenghtening, and you get a `Pack.Foo` module with `type 'a t =
Foo.Map.t`, so those two are compatible.
2. by applying `struct type t = String let compare = compare` directly
instead of naming it `Foo.St`, you apply a module that is not
itself a path, so the typing rules change and you get `'a
Foo.Map.t` abstract as in the first case.
3. You could also define `St` out of `Foo`, so that types in both Foo
and Pack.Foo have `type 'a t = Map.Make(St).t`. You are surely
aware that could similarly use stdlib's `String` directly which
provides a `compare` operation.
I believe this explains the observed behaviour of the type-checker --
the experts will surely correct if I made technical mistakes. I'm not
sure however whether this behavior is expected (or could be considered
slightly buggy), or if it is imposed by theoretical restrictions or
implementation considerations.
On Thu, Mar 1, 2012 at 5:38 PM, Ashish Agarwal <agarwal1975@gmail.com> wrote:
> The following code fails to compile:
>
> ----- a.ml ----
> module Foo = struct
> module St = struct type t = string let compare = compare end
>
> module Map (* : Map.S with type key = St.t *)
> = Map.Make(St)
>
> (* module Map = Map.Make(struct type t = string let compare = compare end)
> *)
> end
>
> module Bar = struct
> type t = int Foo.Map.t
> end
>
> module Pack = struct
> module Foo = Foo
> module Bar = Bar
> end
>
> open Pack
> let x : Bar.t = Foo.Map.empty
> ----
>
> $ ocamlc -c foo.ml
> File "foo.ml", line 20, characters 16-29: (* refers to Foo.Map.empty on last
> line *)
> Error: This expression has type
> 'a Pack.Foo.Map.t = 'a Map.Make(Pack.Foo.St).t
> but an expression was expected of type
> Pack.Bar.t = int Map.Make(Foo.St).t
>
>
> So Pack.Foo and Foo are not compatible. By trial and error, I found two ways
> to resolve the problem:
>
> 1) Provide an explicit signature for Foo.Map (uncomment the provided
> signature), or
> 2) Inline the structure passed to Map.Make (comment out first definition of
> Foo.Map and uncomment the second one)
>
> But I don't understand why. Can anyone explain the main points. Thank you.
>
^ permalink raw reply [flat|nested] 3+ messages in thread