[Caml-list] Question on functors (again...)

["Jocelyn Sérot" <Jocelyn.SEROT@univ-bpclermont.fr>]

Hi,

Following the answer to my question on higher-order functors (https://sympa.inria.fr/sympa/arc/caml-list/2014-01/msg00123.html 
), i've stumbled on another problem, which probably shows that i'm  
definitely missing sth concerning functors.

In the proposed solution, the functor computing the cartesian product  
of two sets was taking as arguments the modules describing the  
_elements_ of the sets.
My idea was to write another functor taking as arguments the sets  
themselves, so that we could build the product of two sets S1 and S2  
with :

module S12 = MakeProduct (S1) (S2) (C)

where S1 and S2 have been defined, for example, with

module S1 = Make(struct type t = int ... end)
module S2 = Make(struct type t = bool ... end)

and C the functor defining the combination of elements of S1 and S2.

I've wrote several versions of this but inevitably bumps on a type  
unfication. By expurging the code progressively, i think the problem  
i'm encountering is best shown in the simplified example below :

To simplify, we will consider a very very minimal description of a  
set, with only two operations : choose and singleton.

The MakeProduct

module type SET = sig
   type t
   type elt
   module Elt : ELT
   val choose: t -> elt
   val singleton: elt -> t
end

The included module Elt is needed since the  MakeProduct functor will  
need to retrieve the type of the elements of its arguments.
The actual implementation of the sets does not matter here; let's take  
a simple list :

module Make (E : ELT) : SET with type elt = E.t and module Elt = E =
struct
   type elt = E.t
   type t = elt list
   module Elt = E
   let choose s = List.hd s
   let singleton e = [e]
end

Let's take an example :

module Int = struct type t = int end
module M1 = Make (Int)
module Bool = struct type t = bool end
module M2 = Make (Bool)

So far so good.

Now the product. For this we extend the signature of elements and sets  
to include a product function :

module type SET_PROD = sig
   include SET
   type t1
   type t2
   val product: t1 -> t2 -> t
end

module type ELT_PROD = sig
   include ELT
   type t1
   type t2
   val product: t1 -> t2 -> t
end

We also need a functor for computing the product of elements. For  
cartesian product this is just :

module MakePair (E1: ELT) (E2: ELT)
   : ELT_PROD with type t1 = E1.t and type t2 = E2.t and type t = E1.t  
* E2.t =
struct
   type t = E1.t * E2.t
   type t1 = E1.t
   type t2 = E2.t
   let product x y = x,y
end

Now, my implementation of the MakeProduct functor :

module MakeProduct
     (S1: SET)
     (S2: SET)
     : SET_PROD
       with type t1 = S1.t
       and type t2 = S2.t
       and type  t = Make(MakePair(S1.Elt)(S2.Elt)).t
       and type elt = MakePair(S1.Elt)(S2.Elt).t
       and type Elt.t = MakePair(S1.Elt)(S2.Elt).t =
struct
   module R = Make(MakePair(S1.Elt)(S2.Elt))
   include R
   type t1 = S1.t
   type t2 = S2.t
   module P = MakePair (S1.Elt) (S2.Elt)
   let product s1 s2 = R.singleton (P.product (S1.choose s1)  
(S2.choose s2))
end

The definition of the product function is obviously wrong (!) but this  
does not matter here.
The pb is that the compiler complains that, in this line, the   
expression ["S1.choose s1"]
has type S1.elt but an expression was expected of type P.t1 = S1.Elt.t

I was expecting that the constraints in the definition of the Make  
functor (".. with type elt=E.t and module Elt =E") would automatically  
enforce the type equality "elt = Elt.t" for all modules defined by  
applying Make (such as S1 and S2). This is obviously not the case. I  
just can't see how to enforce this..

Again, any help on this - probably trivial - issue would be  
appreciated ;-)

Thanks

Jocelyn