From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q4BA4J3i006257 for ; Fri, 11 May 2012 12:04:19 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AhgCAH3jrE/RVaG2kGdsb2JhbABEhXauJQgiAQEBAQkJDRsEI4IuAg8EGQESJwMNBRA3AiQSAQUBIjWHXgMLmVOCXgkDi1SDQ4VBJw2JTQEFC5ARgRgElX2OYD2BWII2 X-IronPort-AV: E=Sophos;i="4.75,570,1330902000"; d="scan'208";a="143455507" Received: from mail-gg0-f182.google.com ([209.85.161.182]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-MD5; 11 May 2012 12:04:13 +0200 Received: by ggnm2 with SMTP id m2so2525901ggn.27 for ; Fri, 11 May 2012 03:04:12 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:sender:from:date:x-google-sender-auth:message-id :subject:to:content-type; bh=qtnsNsM/hW1Yo34el6dcuDMqI56sjfMIUVJ2skVgoZE=; b=TWSF9HnkeUYJkZ3j635Ut6SwONsnP4cACYgDgSEB4xv0loZjQNKSWNAPPkVGExOyjS a1e3EJli/jCtdPbMdM2rSf7s63oMfoed7R8fqWfpCBZXuvW0PtwCQJbb+Ia/MI8dqz8q rAm9GwZjQwFIu9MVLq3/NwGS4hEhykSB89Uro521mzlTLeks4kk8XfrG7JLpruPWFZ5c P7jOsBYTFyOBMaFUYJnQKVLLQnaL3SQuhvsNvKGciZ7A8df6j4hpFAtCa3S+dGPdYJqG g4zO4KVQm3ypAGuGlybznWahExhNtqeeQO1IMVWwvGOmq2tZvBMhMsgJDHrwPiJTObf0 cXgA== Received: by 10.42.63.80 with SMTP id b16mr4252939ici.29.1336730652624; Fri, 11 May 2012 03:04:12 -0700 (PDT) MIME-Version: 1.0 Sender: arnaud.spiwack@gmail.com Received: by 10.64.38.6 with HTTP; Fri, 11 May 2012 03:03:32 -0700 (PDT) From: Arnaud Spiwack Date: Fri, 11 May 2012 12:03:32 +0200 X-Google-Sender-Auth: B2kFqXl42AOnG8utElWD7WhN_yg Message-ID: To: OCaML Mailing List Content-Type: multipart/alternative; boundary=90e6ba5bb94fb5c6df04bfbfdb6e Subject: [Caml-list] One-value functors --90e6ba5bb94fb5c6df04bfbfdb6e Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Dear all, With the advent of first-class modules, I find myself more and more wanting to write functors with only one (value) component, just to benefit from type dependencies. Here is an example (randomly) extracted from Oleg Kiselyov and Jeremy Yallop: type a and b > module type TC =3D sig type 'a t end > module type Subst =3D functor (A:TC) -> sig val x : a A.t -> b A.t end > If this pattern had to become widespread, it would be worth agreeing for a name on the single component, though it's a bit unnecessary to need a name at all. It get very verbose, though, when trying to applying the functor. Supposing I have a module Subst:Subst : let module S =3D Subst(sig type 'a t =3D 'a list) in > S.x =E2=80=A6 > Nothing terrible really, but it sort of gets in the way. I can see benefit in having a special syntax for this sort of definition. I think we could take advantage of first-class functors to get something quite modular, here is a mockup syntax: We could have the type (X:A) =3D> t > stand for (something like) module F =3D functor (X:A) -> sig val x : t end > (module F) > and the definition let f {{X:A}} =3D e > stand for let f =3D let module F (X:A) -> struct let x =3D e end > and finally we'd need an application e {{M}} > would stand for (something like) let module F =3D (val e) in let module F' =3D F(M) in F'.x > Clearly the application needs something like OCaml 4.0 and the type definition some kind of cleverness (I don't know, by the way, why the syntax for F cannot be inlined in the type). In this example syntax the above example would look like type a and b > module type TC =3D sig type 'a t end > val subst : (A:TC) =3D> a A.t -> b B.t > > subst {{sig type 'a t =3D 'a list end}} =E2=80=A6 > I believe this would be something cool to have, so I came with two questions: 1/ Is there some demand for this kind of things (if not, I'm not sure it's worth pursuing, though of course demand could appear after supply) 2/ I don't see how to define the type syntax in camlp4, because of the inlining thing, could it be done? (an alternative may be to have (X:A) =3D> t be a module type, but then (X:A) =3D> (Y:B) =3D> t is not a valid type, so we would need syntaxes for n-ary abstraction/applications) --90e6ba5bb94fb5c6df04bfbfdb6e Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Dear all,

With the advent of first-class modules, I find myself more= and more wanting to write functors with only one (value) component, just t= o benefit from type dependencies. Here is an example (randomly) extracted f= rom Oleg Kiselyov and Jeremy Yallop:

type a and b
modul= e type TC =3D sig type 'a t end
module type Subst =3D functor (A:TC)= -> sig val x : a A.t -> b A.t end

If this pattern had to become widespread, it would be wort= h agreeing for a name on the single component, though it's a bit unnece= ssary to need a name at all.
It get very verbose, though, when trying to= applying the functor. Supposing I have a module Subst:Subst :

let module S =3D Subs= t(sig type 'a t =3D 'a list) in
S.x =E2=80=A6
Nothing terrible really, but it sort of gets in the way. I can see benefi= t in having a special syntax for this sort of definition. I think we could = take advantage of first-class functors to get something quite modular, here= is a mockup syntax:

We could have the type

(X:A) =3D> t

stand for (something like)
=
module F =3D functor (X:A= ) -> sig val x : t end
(module F)

and the definition

let f {{X:A}} =3D e

stand for

let = f =3D let module F (X:A) -> struct let x =3D e end

a= nd finally we'd need an application

e {{M}}

would stand for (something like)

let module F =3D (val e) in let module F' =3D F(M) in F'.x


Clearly the application needs something like OCaml 4.0 and = the type definition some kind of cleverness (I don't know, by the way, = why the syntax for F cannot be inlined in the type).

In this example syntax the above example would look like

type a and b
module type TC =3D sig type 'a t end
val subst : (A:TC) =3D> a A.= t -> b B.t

subst {{sig type 'a t =3D 'a list end}} =E2=80= =A6

I believe this would be something cool to have, so = I came with two questions:
1/ Is there some demand for this kind of things (if not, I'm not sure i= t's worth pursuing, though of course demand could appear after supply)<= br>2/ I don't see how to define the type syntax in camlp4, because of t= he inlining thing, could it be done?
=C2=A0=C2=A0 (an alternative may be to have (X:A) =3D> t be a module typ= e, but then=C2=A0 (X:A) =3D> (Y:B) =3D> t is not a valid type, so we = would need syntaxes for n-ary abstraction/applications)

--90e6ba5bb94fb5c6df04bfbfdb6e--