Piece composition of signatures (& problems derived from them too!)

Piece composition of signatures (& problems derived from them too!)

[Francisco J. Valverde Albacete]

Salut, *Caml* List,

(* version francaise affreuse a` la fin *)

I have been working on deriving a hierarchy of module signatures and 
modules (not classes!) for the benefit of the community (and mine I 
expect).

Trying to mimic this description as undertaken by specification 
formalisms I have been trying to build signatures by piecewise 
composition (believe me, this might have some interest):

(* defining a partial order *)
module type ORDER =
sig
	type t
	val (<=) : t -> t -> bool
end;;

(* defining a total order *)
# module type TOTAL =
sig
	type t
	val compare : t -> t -> int
end;;

        module type TOTAL = sig type t val compare : t -> t -> int end
 
# module type MIXED =
  sig
  	include ORDER
  	include TOTAL with type t = t (* THIS IS THE PROBLEM *)
  end;;

module type MIXED =
  sig
    type t
    val <= : t -> t -> bool
    type t = t
    val compare : t -> t -> int
  end

#module  IntegerMixed : MIXED =
struct
	type t = int
	let (<=) = (<=)
	let compare = (-)
end;;

Characters 31-91:
Signature mismatch:
Modules do not match:
  sig
    type t = int
    val <= : 'a -> 'a -> bool
    val compare : int -> int -> int
  end
is not included in
  MIXED
Type declarations do not match: type t = int is not included in type t = 
t

The problem seems to be that the second "t" hides the first or the type 
equation t = int vanishes.

Has anybody tried and do something remotely resembling this? Any 
remarks/suggestions?

--------------------------------------------------------
J'essaye de composer des signatures des modules (les classes ne son point 
question ici) morceaux par morceaux, jusque comme on fait avec les 
langages d'especification formelle.

svp, voyez les exemples en haut.

Le proble`me me semble etre que le deuxie`me "t" cache le premier ou bien 
que l'equation de type t = int disparait.

Est-ce qu'il y a quelqu'un que ait essaye de faire quelque chose 
semblable? Commentaires/alternatifs?

-- 
Francisco J. Valverde Albacete
Ayudante de Universidad
Area de Tecnolog'ia Electr'onica
Dpto. de Ingenier'ia
Universidad Carlos III de Madrid

e-mail: fva@ing.uc3m.es
tel: 624 94 29
fax : 624 94 30

Re: Piece composition of signatures (& problems derived from them too!)

[Wolfgang Lux]

> # module type MIXED =
>   sig
> 	  include ORDER
> 	  include TOTAL with type t = t (* THIS IS THE PROBLEM *)
>   end;;
> 
> module type MIXED =
>   sig
>     type t
>     val <= : t -> t -> bool
>     type t = t
>     val compare : t -> t -> int
>   end
> 
> Characters 31-91:
> Signature mismatch:
> Modules do not match:
>   sig
>     type t = int
>     val <= : 'a -> 'a -> bool
>     val compare : int -> int -> int
>   end
> is not included in
>   MIXED
> Type declarations do not match: type t = int is not included in type t = 
> t
> 
> The problem seems to be that the second "t" hides the first or the type 
> equation t = int vanishes.

I suspect neither of your assumptions is correct. The problem is that
your module type MIXED includes two(!) type variables named t (look
carefully at the output of the compiler) while your implementation
only provides one. Probably the compiler should already flag your
definition of MIXED as an error because the name t is defined twice in
the environment. (BTW try to enter the expande of the compiler into the
compiler and it will happily barf on you :-)

Regards
Wolfgang

----
Wolfgang Lux
WZH Heidelberg, IBM Germany             Internet: lux@heidelbg.ibm.com
+49-6221-59-4546                        VNET:     LUX at HEIDELBG
+49-6221-59-3500 (fax)	                EARN:     LUX at DHDIBMIP