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

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

[Jocelyn Sérot]

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

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

[Leo White]

Jocelyn Sérot <Jocelyn.SEROT@univ-bpclermont.fr> writes:

> 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..

The compiler doesn't know that your `S1` and `S2` arguments have been
made with the `Make` functor so it cannot assume those constraints. You
should add the constraints to the `SET` module type itself:

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

You've simplified your example, so there may be important complexity
that you've left out, but your code seems to be unnecessarily
complicated. You can probably simplify it to something that looks more
like the code below.

Regards,

Leo

    module type ELT = sig type t end
   
    module type SET = sig
      type t
      type elt
      val choose: t -> elt
      val singleton: elt -> t
    end
   
    module Make (E : ELT) : SET with type elt = E.t = struct
      type elt = E.t
      type t = elt list
      module Elt = E
      let choose s = List.hd s
      let singleton e = [e]
    end
   
    module MakePair (E1: ELT) (E2: ELT) : sig
      include ELT with type t = E1.t * E2.t
      val product : E1.t -> E2.t -> t
    end = struct
      type t = E1.t * E2.t
      let product x y = x,y
    end
   
    module MakeProduct (S1: SET) (S2: SET) : sig 
      include SET with type elt = S1.elt * S2.elt
      val product : S1.t -> S2.t -> t
    end = struct
      module P = MakePair(struct type t = S1.elt end)(struct type t = S2.elt end)
      module S = Make(P)
      include S
      let product s1 s2 = S.singleton (P.product (S1.choose s1) (S2.choose s2))
    end

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

[SEROT Jocelyn]

Thanks for your answer, Leo.

Leo White <lpw25@cam.ac.uk> a écrit :
>

> You should add the constraints to the `SET` module type itself:
>
>     module type SET = sig
>       type t
>       type elt
>       module Elt : sig type t = elt end
>       val choose : t -> elt
>       val singleton : elt -> t
>     end

Unfortunately, this is not possible since the ELT signature is  
actually more complex than just 'sig type t end'.
To illustrate this, without showing the original code (which, as you  
guessed it, has some extra and maybe unrelated complexity), i've tried  
to reuse your example, by simply changing

module type ELT = sig type t end

by

module type ELT = sig type t val string_of: t -> string end

Here's my attempt :

module type ELT =
sig
   type t
   val string_of: t -> string
end

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

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

module MakePair (E1: ELT) (E2: ELT) : sig
   include ELT with type t = E1.t * E2.t
   val product : E1.t -> E2.t -> t
end = struct
   type t = E1.t * E2.t
   let product x y = x,y
   let string_of (x,y) = "(" ^ E1.string_of x ^ "," ^ E2.string_of y ^ ")"
end

module MakeProduct (S1: SET) (S2: SET) : sig
   include SET with type elt = S1.elt * S2.elt
   val product : S1.t -> S2.t -> t
end = struct
   module P = MakePair(S1.Elt)(S2.Elt)
   module S = Make(P)
   include S
   let product s1 s2 = S.singleton (P.product (S1.choose s1) (S2.choose s2))
end

Again, the compiler chokes on the definition of MakeProduct.product,  
saying, for "S1.choose s1", that :

    "This expression has type S1.elt but an expression was expected of  
type S1.Elt.t"

I understand your comment :

> The compiler doesn't know that your `S1` and `S2` arguments have been
> made with the `Make` functor so it cannot assume those constraints.

so, let's add these constraints directly to the functor arguments :

module MakeProduct (S1: SET with type elt = Elt.t) (S2: SET with type  
elt = Elt.t) : sig

but then, we get :

"  module MakeProduct (S1: SET with type elt = Elt.t) (S2: SET) : sig
                                               ^^^^^ Error: Unbound module Elt"

??? The Elt module is part of the SET signature, isn't it ?

Jocelyn

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

[Josh Berdine]

On Tue, Jan 21 2014, SEROT Jocelyn wrote:
> Leo White <lpw25@cam.ac.uk> a écrit :
>>
>> You should add the constraints to the `SET` module type itself:
>>
>>     module type SET = sig
>>       type t
>>       type elt
>>       module Elt : sig type t = elt end
>>       val choose : t -> elt
>>       val singleton : elt -> t
>>     end
>
> Unfortunately, this is not possible since the ELT signature is  
> actually more complex than just 'sig type t end'.
> To illustrate this, without showing the original code (which, as you  
> guessed it, has some extra and maybe unrelated complexity), i've tried  
> to reuse your example, by simply changing
>
> module type ELT = sig type t end
>
> by
>
> module type ELT = sig type t val string_of: t -> string end

Shouldn't Elt.t and elt in SET be equal?  The following typechecks,
though maybe not what you want:

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

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

> module Make (E : ELT) : SET with module Elt = E and type elt = E.t = struct
>    type elt = E.t
>    type t = elt list
>    module Elt = E
>    let choose s = List.hd s
>    let singleton e = [e]
>    let string_of s = "{" ^ E.string_of (choose s) ^ "}"
> end
>
> module MakePair (E1: ELT) (E2: ELT) : sig
>    include ELT with type t = E1.t * E2.t
>    val product : E1.t -> E2.t -> t
> end = struct
>    type t = E1.t * E2.t
>    let product x y = x,y
>    let string_of (x,y) = "(" ^ E1.string_of x ^ "," ^ E2.string_of y ^ ")"
> end
>
> module MakeProduct (S1: SET) (S2: SET) : sig
>    include SET with type elt = S1.elt * S2.elt
>    val product : S1.t -> S2.t -> t
> end = struct
>    module P = MakePair(S1.Elt)(S2.Elt)
>    module S = Make(P)
>    include S
>    let product s1 s2 = S.singleton (P.product (S1.choose s1) (S2.choose s2))
> end

module MakeProduct (S1: SET) (S2: SET) : sig
   include SET with type Elt.t = S1.elt * S2.elt
   val product : S1.t -> S2.t -> t
end = struct
   module P = MakePair(S1.Elt)(S2.Elt)
   module S = Make(P)
   include S
   let product s1 s2 = S.singleton (P.product (S1.choose s1) (S2.choose s2))
end


Cheers, Josh

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

[SEROT Jocelyn]

Josh Berdine <josh@berdine.net> a écrit :
>
> Shouldn't Elt.t and elt in SET be equal?  The following typechecks,
> though maybe not what you want:
>
>> [...]
>
> Cheers, Josh

Thanks a lot Josh !

The magic line to add was :

    type elt = Elt.t

in the SET signature..

This is so obvious afterwards that i should have thought about it  
right from the start (as often...) ;-)

For those interested, here are the signature and implementation of a  
set module extending that provided in the std lib with a cartesian  
product operation (in fact two product ops) and a "string_of" op.

Thx again.

Best wishes

Jocelyn


(* mset.mli *)

module type ELT =
sig
   include Set.OrderedType
   val string_of: t -> string
end

module type SET = sig
   module Elt : ELT
   include Set.S with type elt = Elt.t
   val of_list: elt list -> t
   val string_of: t -> string
end

(* The [Make] functor builds an implementation of a Set given an  
implementation of its elements *)

module Make (E : ELT) : SET with module Elt = E and type elt = E.t

(* The [MakeProduct] functor builds an implementation the cartesian  
product of two sets *)

module MakeProduct (S1: SET) (S2: SET) :
sig
   include SET with type Elt.t = S1.elt * S2.elt
   val product : S1.t -> S2.t -> t
end

(* This is the signature of the last argument to the [MakeProduct'] functor.
    It describes how to build the product of two set elements *)

module type MakePair =
      functor (E1: ELT)
   -> functor (E2: ELT)
   -> sig
        include ELT with type t = E1.t * E2.t
        val product : E1.t -> E2.t -> t
      end

(* The [MakeProduct'] higher-order functor builds a customized  
implementation of the cartesian products of two sets
    when the product of the respective set elements is explicitely  
specified with a dedicated [MakePair] functor *)
(* Note: the [MakeProduct] functor is just a specialization of  
[MakeProduct'] *)

module MakeProduct'
   (S1: SET)
   (S2: SET)
   (F: MakePair) :
sig
   include SET with type Elt.t = S1.elt * S2.elt
   val product : S1.t -> S2.t -> t
end

(* mset.ml *)

module type ELT =
sig
   include Set.OrderedType
   val string_of: t -> string
end

module type SET = sig
   module Elt : ELT
   include Set.S with type elt = Elt.t
   val of_list: elt list -> t
   val string_of: t -> string
end

let string_of_list sep f s =
   let rec h = function
     [] -> ""
   | [x] -> f x
   | x::xs -> f x ^ sep ^ h xs in
   h s

module Make (E : ELT) : SET with module Elt = E and type elt = E.t = struct
   module Elt = E
   module S = Set.Make(E)
   include S
   let string_of s = "{" ^ string_of_list "," E.string_of (S.elements s) ^ "}"
   let of_list l = List.fold_left (fun s e -> S.add e s) S.empty l
end

module type MakePair =
      functor (E1: ELT)
   -> functor (E2: ELT)
   -> sig
        include ELT with type t = E1.t * E2.t
        val product : E1.t -> E2.t -> t
      end

module MakeProduct'
   (S1: SET)
   (S2: SET)
   (F: MakePair) :
sig
   include SET with type Elt.t = S1.elt * S2.elt
   val product : S1.t -> S2.t -> t
end = struct
   module P = F(S1.Elt)(S2.Elt)
   module S = Make(P)
   include S
   let product s1 s2 =
     let f x y t = S.add (P.product x y) t in
     let g x t = S2.fold (f x) s2 t in
     S1.fold g s1 S.empty
end

module MakeProduct (S1: SET) (S2: SET) =
   MakeProduct'
     (S1)
     (S2)
     (functor (E1: ELT) -> functor (E2: ELT) -> struct
       type t = E1.t * E2.t
       let compare = Pervasives.compare
       let product x y = x,y
       let string_of (x,y) = "(" ^ E1.string_of x ^ "," ^ E2.string_of y ^ ")"
     end)

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

[Leo White]

> Unfortunately, this is not possible since the ELT signature is  actually more complex than just 'sig type t end'.
> To illustrate this, without showing the original code (which, as you  guessed it, has some extra and maybe unrelated
> complexity), i've tried  to reuse your example, by simply changing

You can still add the constraint to the SET type:

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

You should also remove the equivalent constraint from the `Make`
functor:
   
  module Make (E : ELT) : SET with type elt = E.t = struct
    type elt = E.t
    type t = elt list
    module Elt = E
    let choose s = List.hd s
    let singleton e = [e]
    let string_of s = "{" ^ E.string_of (choose s) ^ "}"
  end

Regards,

Leo