Re: functors and type constraints

[Jocelyn Serot <jserot@epcc.ed.ac.uk>]

Hello,

In his last post, P. Boulet <Pierre.Boulet@prism.uvsq.fr> says:

> hello,
> 
> I have a problem with some complicated type constraints with Objective
> Caml version 1.02. Let have an example:
> 
> [stuff deleted]
> 
> Everything goes find till now. Let's instanciate the modules now.
> 
> module T1 : TAG  struct ... end;;
> module T2 : TAG  struct ... end;;
> module A1 : ARBRE  Make_arbre (T1);;
> module A2 : ARBRE  Make_arbre (T2);;
> module Trad_Tag : TRAD  =
> 
>   struct =
> 
>     type from  T1.t
>     type into  T2.t
>     val f ... =
> 
>   end;;
> 
> The problem appears during the compilation of the following statement:
> module Trad_Arbre : TRAD  Make_trad (A1) (A2) (Trad_Tag);;
> Signature mismatch:
> Modules do not match:
>   sig =
>     type from  Trad_Tag.from =
>     type into  Trad_Tag.into =
>     val f : from -> into =
>   end
> is not included in
>   sig type from  A1.tag type into  A2.tag val f : from -> into end
> Type declarations do not match:
>   type from  Trad_Tag.from
> is not included in
>   type from  A1.tag
> 
> These types are equal though. I imagine a problem of abstract
> definition of some types, but how can I signify to the compiler that
> these types are equal?

I understand your problem as follows: given a function f to convert between
TAGs, you want to build a function to convert between ARBREs.

I recently came across a very similar problem dealing, respectively,
with PIXELs and IMAGEs.
Here's the solution i finally wrote, adapted a bit to fit to your definitions:

----------------------------- trad.ml ------------------------------------------

module type TAG = sig type t end;;

module type ARBRE = sig type tag type quast end;;

module type MAKE_ARBRE = 
  functor (T : TAG) -> (ARBRE with type tag = T.t);;

module Make_arbre : MAKE_ARBRE =
  functor (T : TAG) -> 
    struct
      type tag = T.t
      type quast = {tag : tag}
    end;;

module type TRAD = sig type t1 type t2 val f : t1 -> t2 end;;

module type Make_trad = functor
	(A1 : ARBRE) -> functor
	(A2 : ARBRE) -> functor
	(F  : sig val f : A1.tag -> A2.tag end)
	-> TRAD with type t1 = A1.tag and type t2 = A2.tag;;

module T1 : TAG = struct type t = float end;;
module T2 : TAG = struct type t = int end;;
module A1 : ARBRE = Make_arbre(T1);;
module A2 : ARBRE = Make_arbre(T2);;

module Trad = Make_trad (A1) (A2) (struct let f = truncate end);;

----------------------------- trad.ml ------------------------------------------

Hope that helps.

-------------------------------------------------------------------------------
E-mail: jserot@epcc.ed.ac.uk (->Nov 29 1996) ................................
S-mail: LASMEA - URA 1793 CNRS, Universite Blaise Pascal, 63177 Aubiere cedex
Tel: (33) 73.40.73.30 - Fax: (33) 73.40.72.62 ...............................
.... http://wwwlasmea.univ-bpclermont.fr/Personnel/Jocelyn.Serot/Welcome.html
-------------------------------------------------------------------------------