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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 2C68A7F02D for ; Tue, 21 Oct 2014 10:52:46 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of arnaud.spiwack@gmail.com) identity=pra; client-ip=74.125.82.41; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="arnaud.spiwack@gmail.com"; x-sender="arnaud.spiwack@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of arnaud.spiwack@gmail.com designates 74.125.82.41 as permitted sender) identity=mailfrom; client-ip=74.125.82.41; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="arnaud.spiwack@gmail.com"; x-sender="arnaud.spiwack@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-wg0-f41.google.com) identity=helo; client-ip=74.125.82.41; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="arnaud.spiwack@gmail.com"; x-sender="postmaster@mail-wg0-f41.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: At8BAFsXRlRKfVIplGdsb2JhbABchDkEgwLRZgcWAREBAQEBBwsLCRIwhBsRBBkBOQMNBQkHNwIkEgEFASIbEweICQMRn22DHW6LMIUCiQ8nDYZUAQUOk0GBVAEEnVqULRgpgW+BDAELgiY7L4JLAQEB X-IPAS-Result: At8BAFsXRlRKfVIplGdsb2JhbABchDkEgwLRZgcWAREBAQEBBwsLCRIwhBsRBBkBOQMNBQkHNwIkEgEFASIbEweICQMRn22DHW6LMIUCiQ8nDYZUAQUOk0GBVAEEnVqULRgpgW+BDAELgiY7L4JLAQEB X-IronPort-AV: E=Sophos;i="5.04,760,1406584800"; d="scan'208";a="102173782" Received: from mail-wg0-f41.google.com ([74.125.82.41]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 21 Oct 2014 10:52:45 +0200 Received: by mail-wg0-f41.google.com with SMTP id b13so776565wgh.0 for ; Tue, 21 Oct 2014 01:52:43 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:sender:from:date:message-id:subject:to:content-type; bh=n+xwIeWXSrrA+XSaRRSHcd8hBIe6l+4RbA+4FAXnnhM=; b=gCp7Aa6X7RNIz5eOLZkz1QhHNnb1gsxKVIDY2r12lR6Ixk5PPOkMt+UcJSleY7+K75 2AgbW17Dg7iHz4Sg0RGWH0Fsv8Cp6ymb/Tn6j7yV64eFHQlagEiwKMeKoIAFYEuEUz3s O1SWIXokMwdw9avwMAnDNu2RBKdtztGzCZL4GVRbkrX+pNh5mMlQ8mcW6J4SG3iRK2cM rgLYXvu9OJ832jYq96WAHhtiq7Po/BR06ecjXazm126KrGdJPlNXRyV8RNAmBKUY9O75 2QMsgYbx2UJ/P4rqtX7Iuq3dQdsXEjKD6NSBgtloP9TtwB6bWESt68fqwaW63a4TRZmv 4epQ== X-Received: by 10.180.103.233 with SMTP id fz9mr26436163wib.80.1413881562848; Tue, 21 Oct 2014 01:52:42 -0700 (PDT) MIME-Version: 1.0 Sender: arnaud.spiwack@gmail.com Received: by 10.216.57.4 with HTTP; Tue, 21 Oct 2014 01:52:02 -0700 (PDT) From: Arnaud Spiwack Date: Tue, 21 Oct 2014 10:52:02 +0200 X-Google-Sender-Auth: bnFM4W3aUFtNWAyj4C0x68q0rqo Message-ID: To: OCaML Mailing List Content-Type: multipart/alternative; boundary=f46d044280ca4ee2560505eaf41d X-Validation-by: arnaud@spiwack.net Subject: [Caml-list] Manipulating Modules Modularly --f46d044280ca4ee2560505eaf41d Content-Type: text/plain; charset=UTF-8 Dear all, Here is a puzzle I run way to often in (yesterday was one of these) and have not good solution to. Suppose I have a module signature such as monoids: module type M = sig type t val u:t val p:t->t->t end And a functor: module type ME = sig type t val ps:t list -> t end module ME (M:M) : ME with type t := M.t All good and well. I now want to reuse my functor for list, which are a monoid. But I can only get: module type TYPE = sig type t end module LEF (T:TYPE) : ME with type t = T.t list By the way, I have no intuition why I cannot use a := (substitution) above and am stuck with a type definition. But that's not my question. What I really want is a module module LE : ME with type t := 'a list There are two problems here. First, I don't know how to define the signature (which, expanded would be sig val ps : 'a list list -> 'a list) without copying. Second I don't know how to do write the module LE itself, without boilerplate proportional to the number of function in the signature. With local modules it is reasonably easy to implement LE without modifying ME, by re-exporting every function as a function which instantiates LEF (though I guess [u] would only work because list is covariant). But I would rather the module LE to extend automatically as I extend the signature of ME. The thing is, this is just the commutation between forall-s and product-s. So provided the functor instantiation is pure, then it is always possible to do that. But I don't know of any modular way to do it. So here's my question: how do you/would you solve this problem. If the solution is compatible with 3.12, it's a plus. /Arnaud --f46d044280ca4ee2560505eaf41d Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
Dear all,

Here is a puzzle I run way to often in (y= esterday was one of these) and have not good solution to.

Suppose I = have a module signature such as monoids:

module type M =3D sig=C2=A0 type t=C2=A0 val u:t=C2=A0 val p:t->t-&= gt;t=C2=A0 end

And a functor:

module type ME =3D sig=C2=A0 type t=C2=A0 val ps:t list -> t=C2= =A0 end
module ME (M:M) : ME with type t :=3D M.t

All good = and well. I now want to reuse my functor for list, which are a monoid. But = I can only get:

module type TYPE =3D= sig type t end
module LEF (T:TYPE) : ME with type t =3D T.t list

By the way, I have no intuition why I cannot use a :=3D (substitutio= n) above and am stuck with a type definition.

But that's not my = question. What I really want is a module

module LE : ME with type t :=3D 'a list

There are two= problems here. First, I don't know how to define the signature (which,= expanded would be =C2=A0 sig val ps : 'a list list -> 'a list) = without copying. Second I don't know how to do write the module LE itse= lf, without boilerplate proportional to the number of function in the signa= ture.

With local modules it is reasonably easy to implement LE witho= ut modifying ME, by re-exporting every function as a function which instant= iates LEF (though I guess [u] would only work because list is covariant). B= ut I would rather the module LE to extend automatically as I extend the sig= nature of ME.

The thing is, this is just the commutation between for= all-s and product-s. So provided the functor instantiation is pure, then it= is always possible to do that. But I don't know of any modular way to = do it.

So here's my question: how do you/would you solve this pr= oblem. If the solution is compatible with 3.12, it's a plus.


/Arnaud
--f46d044280ca4ee2560505eaf41d--