Extending Set - strange behavior of abstract type

Extending Set - strange behavior of abstract type

[Dawid Toton]

I tried to extend the standard Set module with new operations. I got 
error messages about type incompatibilities (the Set.S.t as exposed by 
my implementation and Set.S.t used by functions from the original Set). 
I have reduced my code to the following small example:

module Set = struct
   module Make (Ord : Set.OrderedType) = struct
     module Set = Set.Make(Ord)
     include Set
   end
end

module OrdChar = struct type t = char let compare = compare end
module Raw1 = Set.Make (OrdChar)
module Raw2 = Set.Make (struct type t = char let compare = compare end)

let aaa (aa : Raw1.t) (bb : Raw1.Set.t) = (aa = bb)
let aaa (aa : Raw2.t) (bb : Raw2.Set.t) = (aa = bb)

Only the last line results in an error:
Error: This expression has type Raw2.Set.t but is here used with type Raw2.t

All the rest of the code compiles correctly. It means that types Raw1.t 
and Raw1.Set.t can be unified.

My question is: why these nearly identical statements results in 
different behavior of the type t?

I'd really prefer Raw1 and Raw2 to be identical.
I use ocaml 3.11.0.

Dawid

Re: [Caml-list] Extending Set - strange behavior of abstract type

[rossberg]

Dawid Toton <d0@wp.pl> wrote:
> I tried to extend the standard Set module with new operations. I got
> error messages about type incompatibilities (the Set.S.t as exposed by
> my implementation and Set.S.t used by functions from the original Set).
> I have reduced my code to the following small example:
>
> module Set = struct
>    module Make (Ord : Set.OrderedType) = struct
>      module Set = Set.Make(Ord)
>      include Set
>    end
> end
>
> module OrdChar = struct type t = char let compare = compare end
> module Raw1 = Set.Make (OrdChar)
> module Raw2 = Set.Make (struct type t = char let compare = compare end)
>
> let aaa (aa : Raw1.t) (bb : Raw1.Set.t) = (aa = bb)
> let aaa (aa : Raw2.t) (bb : Raw2.Set.t) = (aa = bb)
>
> Only the last line results in an error:
> Error: This expression has type Raw2.Set.t but is here used with type
> Raw2.t

That is a known limitation of Ocaml's module system: type equivalence is
only propagated through a syntactic subset of module expressions, so
called "paths" (which consist of only module names, dot access, and
functor applications).

Roughly, in your example, Raw1.t is just an abbreviation for
Set.Make(OrdChar).t, which in turn abbreviates Set.Make(OrdChar).Set.t,
which expands to Set.Set.Make(OrdChar).t. In all these type names the bits
before the ".t" are in path form, which makes the type expressions legal.

Raw2.t, on the other hand, would expand to Set.Make(struct ... end).t -
however, literal structures are not allowed in paths, so this type
expression is illegal, and Ocaml simply "forgets" the equivalence.

The workaround is never to apply a functor to an anonymous structure if
you care about maximum type propagation. Just name it, which is easy
enough in most cases.

/Andreas

Re: Extending Set - strange behavior of abstract type

[Sylvain Le Gall]

On 27-04-2010, Dawid Toton <d0@wp.pl> wrote:
> I tried to extend the standard Set module with new operations. I got 
> error messages about type incompatibilities (the Set.S.t as exposed by 
> my implementation and Set.S.t used by functions from the original Set). 
> I have reduced my code to the following small example:
>
> module Set = struct
>    module Make (Ord : Set.OrderedType) = struct
>      module Set = Set.Make(Ord)
>      include Set
>    end
> end
>
> module OrdChar = struct type t = char let compare = compare end
> module Raw1 = Set.Make (OrdChar)
> module Raw2 = Set.Make (struct type t = char let compare = compare end)
>
> let aaa (aa : Raw1.t) (bb : Raw1.Set.t) = (aa = bb)
> let aaa (aa : Raw2.t) (bb : Raw2.Set.t) = (aa = bb)
>
> Only the last line results in an error:
> Error: This expression has type Raw2.Set.t but is here used with type Raw2.t
>
> All the rest of the code compiles correctly. It means that types Raw1.t 
> and Raw1.Set.t can be unified.
>
> My question is: why these nearly identical statements results in 
> different behavior of the type t?
>
> I'd really prefer Raw1 and Raw2 to be identical.

You just have to propagate the type by hand:

module Set =
struct
  module Make (Ord : Set.OrderedType) =
    struct
      include Set.Make(Ord)
      module Set : Set.S with type t = t = Set.Make(Ord)
    end
end

The "type t = t" do the trick. The first t is bound inside Set and the other
comes from "include Set.Make(Ord)".

Regards
Sylvain Le Gall