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 9DDCC7F02D for ; Wed, 22 Oct 2014 11:51:52 +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=209.85.212.178; 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 209.85.212.178 as permitted sender) identity=mailfrom; client-ip=209.85.212.178; 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-wi0-f178.google.com) identity=helo; client-ip=209.85.212.178; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="arnaud.spiwack@gmail.com"; x-sender="postmaster@mail-wi0-f178.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AoABANR9R1TRVdSylGdsb2JhbABcDoQsBIMC0jUHFgERAQEBAQcLCwkSMIQDAQEDARIRBBkBOAEDAQsBBQMCBAcDNAICIhIBBQEcBhsaiAoDCQiUJ5A4bosxhQOIdycNhjgBCxoBBQ6TR4FUAQSPZo13gTGQd4IMGCmBb4J9QjsvgksBAQE X-IPAS-Result: AoABANR9R1TRVdSylGdsb2JhbABcDoQsBIMC0jUHFgERAQEBAQcLCwkSMIQDAQEDARIRBBkBOAEDAQsBBQMCBAcDNAICIhIBBQEcBhsaiAoDCQiUJ5A4bosxhQOIdycNhjgBCxoBBQ6TR4FUAQSPZo13gTGQd4IMGCmBb4J9QjsvgksBAQE X-IronPort-AV: E=Sophos;i="5.04,768,1406584800"; d="scan'208";a="102360644" Received: from mail-wi0-f178.google.com ([209.85.212.178]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 22 Oct 2014 11:51:52 +0200 Received: by mail-wi0-f178.google.com with SMTP id r20so814290wiv.17 for ; Wed, 22 Oct 2014 02:51:51 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:sender:in-reply-to:references:from:date:message-id :subject:to:cc:content-type; bh=j3tTuutWuFHJ6dElxpZpPA7i+HXCH8QzG/yBj30qgg4=; b=fNnr5f4qJf45SU9a+Rf5eLpJhE53AofJQr5vD/BJO5ohjTFspwn8TzKNUoCybezFXy mMuBTsQWndTzZAUFlEfFBmW8nbs2sax/yrZ5r6DuUsFpzY6bD22031dHmI3LzRu7/NSu 64j36aadqFdtSvXNDlljbq6qf/faIAlHvUjvMx/UVsorVGcPSqnqWtupGh1gMdNlni1V rcqUG+VHhpVEOk2CGqtTDFZRFf8IHq7r0Rrck0b1dHPym5ION7SOwmjWxM5CiI7IBLas TgvjQsLzsKmoaLkU0mxxFwDX+zrtzZ9MRnDhs8XVVDgKBBnNqLsKcbd3kHJ29SH0beOu mwfQ== X-Received: by 10.194.82.161 with SMTP id j1mr50499124wjy.38.1413971511703; Wed, 22 Oct 2014 02:51:51 -0700 (PDT) MIME-Version: 1.0 Sender: arnaud.spiwack@gmail.com Received: by 10.216.57.4 with HTTP; Wed, 22 Oct 2014 02:51:11 -0700 (PDT) In-Reply-To: <86fveho4p1.fsf@cam.ac.uk> References: <8638ahpq1m.fsf@cam.ac.uk> <86y4s9oah2.fsf@cam.ac.uk> <86fveho4p1.fsf@cam.ac.uk> From: Arnaud Spiwack Date: Wed, 22 Oct 2014 11:51:11 +0200 X-Google-Sender-Auth: 8rd20Fi9CxEb8uanLV3B0QX9Vw4 Message-ID: To: Leo White Cc: OCaML Mailing List Content-Type: multipart/alternative; boundary=047d7bb04bdaad7f200505ffe535 X-Validation-by: arnaud@spiwack.net Subject: Re: [Caml-list] Manipulating Modules Modularly --047d7bb04bdaad7f200505ffe535 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable > Depends which issue you mean. > I mean having a functor which compiles with several signatures and wanting to leverage that fact with minimal fuss. But obviously, it does not seem to stir the passions of the ocaml list readers. I'm going for weird=E2=80=A6 > Note that your problem can also be worked around for a fixed number of > type parameters by defining your module types as: > > module type M =3D sig > type 'a t > val u : 'a t > val p : 'a t -> 'a t -> 'a t > end > > module type ME =3D sig > type 'a t > val ps: 'a t list -> 'a t > end > > which will now work for types with 0 or 1 parameters. > It's not very modular, but indeed. It requires signature duplication however, because (for some reason), we cannot do things like "S with type 'a t :=3D int", and I happen to use substitution. I guess I could use more powerful ways to manipulate signatures. Like taking a module signature with a type [t], and turn it into the same signature of type ['a t] (with 'a universally bound at each function). This is always well defined, isn't it? The other way around sound easier to do however (replacing a Signature on ['a t] by a signature in [t]), as it it just requires loosening the restriction on "same parameters" in member substitution to "a subset of the parameters". But it's less modular and not as good for documentation. But it would be sufficient for many use-cases. That would break a lot of existing code and wouldn't work very well > without a full effect system in the core language. > I don't think it would break that much (and if it breaks something the fix is two characters long=E2=80=A6). I mean, the functions exported by the fun= ctor need not be pure. It's just the functor application which has to (that is no reference or such at toplevel). I don't think an effect system is required for that. But my question is mostly theoretical, anyway. --047d7bb04bdaad7f200505ffe535 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable

=
Depends which issue you mean.

I mean having a functor which compiles with several signatures a= nd wanting to leverage that fact with minimal fuss. But obviously, it does = not seem to stir the passions of the ocaml list readers. I'm going for = weird=E2=80=A6
=C2=A0
Note that your problem can also be worked around for a fixed number of
type parameters by defining your module types as:

=C2=A0 =C2=A0 module type M =3D sig
=C2=A0 =C2=A0 =C2=A0 =C2=A0 type 'a t
=C2=A0 =C2=A0 =C2=A0 =C2=A0 val u : 'a t
=C2=A0 =C2=A0 =C2=A0 =C2=A0 val p : 'a t -> 'a t -> 'a t<= br> =C2=A0 =C2=A0 =C2=A0 end

=C2=A0 =C2=A0 module type ME =3D sig
=C2=A0 =C2=A0 =C2=A0 =C2=A0type 'a t
=C2=A0 =C2=A0 =C2=A0 =C2=A0val ps: 'a t list -> 'a t
=C2=A0 =C2=A0 end

which will now work for types with 0 or 1 parameters.
=
It's not very modular, but indeed. It requires signature duplicatio= n however, because (for some reason), we cannot do things like "S with= type=C2=A0 'a t :=3D int", and I happen to use substitution. I gu= ess I could use more powerful ways to manipulate signatures. Like taking a = module signature with a type [t], and turn it into the same signature of ty= pe ['a t] (with 'a universally bound at each function). This is alw= ays well defined, isn't it?

The other way around sound easier to= do however (replacing a Signature on ['a t] by a signature in [t]), as= it it just requires loosening the restriction on "same parameters&quo= t; in member substitution to "a subset of the parameters". But it= 's less modular and not as good for documentation. But it would be suff= icient for many use-cases.

That would break a lot of existing code and wouldn't work very w= ell
without a full effect system in the core language.
I don't think it would break that much (and if it breaks something the= fix is two characters long=E2=80=A6). I mean, the functions exported by th= e functor need not be pure. It's just the functor application which has= to (that is no reference or such at toplevel). I don't think an effect= system is required for that. But my question is mostly theoretical, anyway= .
--047d7bb04bdaad7f200505ffe535--