From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 1BBA17F6C4 for ; Mon, 20 Jan 2014 17:34:31 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of Jocelyn.SEROT@univ-bpclermont.fr) identity=pra; client-ip=195.221.122.150; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="Jocelyn.SEROT@univ-bpclermont.fr"; x-sender="Jocelyn.SEROT@univ-bpclermont.fr"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of Jocelyn.SEROT@univ-bpclermont.fr) identity=mailfrom; client-ip=195.221.122.150; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="Jocelyn.SEROT@univ-bpclermont.fr"; x-sender="Jocelyn.SEROT@univ-bpclermont.fr"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@ubpmes.univ-bpclermont.fr) identity=helo; client-ip=195.221.122.150; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="Jocelyn.SEROT@univ-bpclermont.fr"; x-sender="postmaster@ubpmes.univ-bpclermont.fr"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AtEBAMtP3VLD3XqWnGdsb2JhbABZg0O9IhYOAQEBAQEIFAk8glMRAoE/Pi6HbgmYVasIEwSRNQ9mgRQEjmCFXJks X-IPAS-Result: AtEBAMtP3VLD3XqWnGdsb2JhbABZg0O9IhYOAQEBAQEIFAk8glMRAoE/Pi6HbgmYVasIEwSRNQ9mgRQEjmCFXJks X-IronPort-AV: E=Sophos;i="4.95,691,1384297200"; d="scan'208";a="45460821" Received: from ubpmes.univ-bpclermont.fr ([195.221.122.150]) by mail3-smtp-sop.national.inria.fr with ESMTP; 20 Jan 2014 17:34:24 +0100 Received: from localhost (localhost.localdomain [127.0.0.1]) by ubpmes.univ-bpclermont.fr (Postfix) with ESMTP id 90A5D75008E1 for ; Mon, 20 Jan 2014 17:34:23 +0100 (CET) X-Virus-Scanned: amavisd-new at univ-bpclermont.fr Received: from ubpmes.univ-bpclermont.fr ([127.0.0.1]) by localhost (ubpmes.univ-bpclermont.fr [127.0.0.1]) (amavisd-new, port 10024) with ESMTP id oKXOWvqTCseo for ; Mon, 20 Jan 2014 17:34:21 +0100 (CET) Received: from dhcpprov120-20.epucfe.eu (unknown [193.54.51.240]) by ubpmes.univ-bpclermont.fr (Postfix) with ESMTP id E67897500C48 for ; Mon, 20 Jan 2014 17:34:21 +0100 (CET) Message-Id: From: =?ISO-8859-1?Q?Jocelyn_S=E9rot?= To: OCaML Mailing List Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Content-Transfer-Encoding: 7bit Mime-Version: 1.0 (Apple Message framework v936) Date: Mon, 20 Jan 2014 17:34:21 +0100 X-Mailer: Apple Mail (2.936) Subject: [Caml-list] Question on functors (again...) 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