Re: [Caml-list] Caml 3.01 : pb with include

[Andreas Rossberg <rossberg@ps.uni-sb.de>]

Christophe Raffalli wrote:
> 
> I tried to use the new include feature for my algebra library. I failed
> !
> Am I missing something ?

Actually it is not the include feature causing the trouble, but rather
your use of with module constraints.

> Here is a small example I created just to show the problem:
> 
> module type Semi_Group =
> sig
>   type t
>   val e : t
>   val ( ** ) : t -> t -> t
> end
> 
> module type Group =
> sig
>   include Semi_Group
>   val inv : t -> t
> end
> 
> module type Semi_Group_Morphism =
> sig
>   module SG1 : Semi_Group
>   module SG2 : Semi_Group
>   val f : SG1.t -> SG2.t
> end
> 
> module type Group_Morphism =
> sig
>   module G1 : Group
>   module G2 : Group
>   include Semi_Group_Morphism with module SG1 = G1 and module SG2 = G2
> end
> 
> (*
> Nice : SG1 et SG2 are groups : Here isCaml answer

Well, not so nice really, because this treatment exactly is what causes
the later error. See below.

> module type Group_Morphism =
>   sig
>     module G1 : Group
>     module G2 : Group
>     module SG1 :
>       sig
>         type t = G1.t
>         val e : t
>         val ( ** ) : t -> t -> t
>         val inv : t -> t
>       end
>     module SG2 :
>       sig
>         type t = G2.t
>         val e : t
>         val ( ** ) : t -> t -> t
>         val inv : t -> t
>       end
>     val f : SG1.t -> SG2.t
> 
> end
> *)
> 
> module Idt_Semi_Group_Morphism(SG : Semi_Group) = (
> struct
>   module SG1 = SG
>   module SG2 = SG
>   let f = fun x -> x
> end : Semi_Group_Morphism with module SG1 = SG and module SG2 = SG)
> 
> module Idt_Group_Morphism(G : Group) = (
> struct
>   module G1 = G
>   module G2 = G
>   include (Idt_Semi_Group_Morphism(G) : Semi_Group_Morphism with module
> SG1 = G and module SG2 = G)
> end : Group_Morphism with module SG1 = G and module SG2 = G and module
> G1 = G and module G2 = G)

Just an aside: some of the outer module constraints here are redundant,
because they are already specified in the signature Group_Morphism. It
should suffice to say:

 ... : Group_Morphism with module G1 = G and module G2 = G

The signature annotation (at the include) also is a bit unnecessary, but
is the one that seems to be causing the error.

> (*
> Heavy and does not work !
> 
> Signature mismatch:
> Modules do not match:
>   sig
>     module SG1 : sig type t = G.t val e : t val ( ** ) : t -> t -> t end
>     module SG2 : sig type t = G.t val e : t val ( ** ) : t -> t -> t end
>     val f : SG1.t -> SG2.t
>   end

That is the result signature of the functor application
Idt_Semi_Group_Morphism(G).

> is not included in
>   sig
>     module SG1 :
>       sig
>         type t = G.t
>         val e : t
>         val ( ** ) : t -> t -> t
>         val inv : t -> t
>       end
>     module SG2 :
>       sig
>         type t = G.t
>         val e : t
>         val ( ** ) : t -> t -> t
>         val inv : t -> t
>       end
>     val f : SG1.t -> SG2.t
>   end

And that is the signature the compiler seems to calculate for

  Semi_Group_Morphism with module SG1 = G and module SG2 = G

Like in the case of Group_morphism above, SG1 and SG2 contain an inv
member in this signature. I think this semantics of module constraints
is not right - it should not extend subsignatures, only propagate type
identities. This not exactly is a bug, but IMHO not what you want in
most situations - at least not in this particular situation. Was there a
particular motivation to design the language this way?

> Modules do not match:
>   sig type t = G.t val e : t val ( ** ) : t -> t -> t end
> is not included in
>   sig type t = G.t val e : t val ( ** ) : t -> t -> t val inv : t -> t
> end
> The field `inv' is required but not
> provided
> *)

And this is correct, given the semantics of module constraints.

The simplest workaround is to remove the signature annotation at the
include spec (did not try it, though). Alternatively, you could avoid
using module constraints and restrict yourself to type constraints, ie.

  include (Idt_Semi_Group_Morphism(G) : Semi_Group_Morphism
           with type SG1.t = G.t and type SG2.t = G.t)

And similar in signature Group_Morphism.

Best regards,

	- Andreas

-- 
Andreas Rossberg, rossberg@ps.uni-sb.de

"Computer games don't affect kids.
 If Pac Man affected us as kids, we would all be running around in
 darkened rooms, munching pills, and listening to repetitive music."
-------------------
To unsubscribe, mail caml-list-request@inria.fr.  Archives: http://caml.inria.fr