From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <arnaud.spiwack@gmail.com>
X-Original-To: caml-list@sympa.inria.fr
Delivered-To: caml-list@sympa.inria.fr
Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82])
	by sympa.inria.fr (Postfix) with ESMTPS id 896E47ED26
	for <caml-list@sympa.inria.fr>; Wed, 30 May 2012 16:14:50 +0200 (CEST)
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: Av8BAFYqxk/RVaCyimdsb2JhbABEhUqlUYhqCCIBAQEKCQ0HEgYjghgBAQQSAg8EGQESJwMMAQUDAgs3AgIiEgEFARwGNYdbAwsLmkMJA4tbg0CFKicNiUgBBQyPKYESA5UYgQ+NBz6BVIIt
X-IronPort-AV: E=Sophos;i="4.75,685,1330902000"; 
   d="scan'208";a="160590550"
Received: from mail-gh0-f178.google.com ([209.85.160.178])
  by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-MD5; 30 May 2012 16:14:49 +0200
Received: by ghbf1 with SMTP id f1so2963242ghb.9
        for <caml-list@inria.fr>; Wed, 30 May 2012 07:14:48 -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
         :x-google-sender-auth:message-id:subject:to:content-type;
        bh=9ph+oVtXas42QSBxmO3wr+QLu/94uZJrT+bGYB7yUCk=;
        b=XOg4PG9NmfQuCNZhuR9SG+f1hXYfGwxwVMustWUsfElqMkfIkulC9n+2uzoVeK0B5t
         fROB7sDpjGlz2ycY9c+cYri66crikh6VBc4Zb5AFE/+YnBgfMgyQCAh6BvELz5sKLKvX
         XC1YcPTcjF87u7sH1L9758c/CCyjfEzN2ld0WjC0XNPuf9tJsh00iGj2HMgQA140Gdnc
         EagEK0ggQNdxDImjBwb5ExHr0m4CQEPgM/qT/FaT/0OY8QrkIzfkZPA2fP3caVTOYpjz
         z056kg5ic7hXVChh5sL9QJZBdd2CohKbdHpjTf3pNDdOlCjgGQu+QjJEeuRTEXQ0qPqG
         lwKA==
Received: by 10.50.161.198 with SMTP id xu6mr10919781igb.40.1338387288335;
 Wed, 30 May 2012 07:14:48 -0700 (PDT)
MIME-Version: 1.0
Sender: arnaud.spiwack@gmail.com
Received: by 10.64.38.6 with HTTP; Wed, 30 May 2012 07:14:08 -0700 (PDT)
In-Reply-To: <CAMoPVjcTRLQzPm09PxLUFvaGWBgG+Spvd6=JJJH590NNe=cRDQ@mail.gmail.com>
References: <CAMoPVjchxsQ5QDdsfBU+TDVmhAxrBUndDNJzVP==WT1vcE8gcw@mail.gmail.com>
 <CA+qp_4qiEQDiEhotX8dY1esLVeXqjorttW9EJLWvWUqmeaXTRQ@mail.gmail.com> <CAMoPVjcTRLQzPm09PxLUFvaGWBgG+Spvd6=JJJH590NNe=cRDQ@mail.gmail.com>
From: Arnaud Spiwack <Arnaud.Spiwack@lix.polytechnique.fr>
Date: Wed, 30 May 2012 16:14:08 +0200
X-Google-Sender-Auth: FCdQYsr87yEL2uQuYxAGs7XgAYg
Message-ID: <CAMoPVjfH-SR7O4p9KFfmFqX-P0rpKKwWkvTAbYOZk-ur4pc6hg@mail.gmail.com>
To: OCaml Mailing List <caml-list@inria.fr>
Content-Type: multipart/alternative; boundary=14dae9341141e4a7ef04c14192de
Subject: Re: [Caml-list] One-value functors


--14dae9341141e4a7ef04c14192de
Content-Type: text/plain; charset=UTF-8

Here is another kind of example I've boiled down as much as I could (it is
somewhat related to the Leibniz equality).
Oleg Kiselyov and Jeremy Yallop (
http://okmij.org/ftp/ML/first-class-modules/ ) have noticed that
first-class modules could be leveraged to produce an variant of the Finally
Tagless approach (which consist in replacing the use of a gadt by a
typeclass signature, in Haskell, to denote expressions). I like to call it
Initially Tagless.

The idea is to start with a signature representing your language, a field
for each language construct. Here, the language admits two types (int and
bool) and one operation on each:

module type S = sig
  type 'a t

  val int : int -> int t
  val bool : bool -> bool t
  val (+) : int t -> int t -> int t
  val if_ : bool t -> 'a t -> 'a t -> 'a t
end

An interpreter for the language is a module of type S. The type of
expressions [a Expr.t] is, then, defined as that of things which, for any
interpretor X, can be interpreted into an [a X.t]. Here goes the code in
OCaml 3.12, you might notice it is very repetitive:

module Expr : sig
  include S

  module Interp (X:S) : sig
    val x : 'a t -> 'a X.t
  end
end = struct

  module type T = sig
    type a

    module Interp (X:S) : sig
      val x : a X.t
    end
  end

  type 'a t = (module T with type a = 'a)

  module Interp (X:S) = struct
    let x (type w) (e:w t) : w X.t=
      let module E = (val e : T with type a = w) in
      let module IE = E.Interp(X) in
      IE.x
  end

  let int x =
    let module M = struct
      type a = int

      module Interp (X:S) = struct
        let x = X.int x
      end
    end in
    (module M : T with type a = int)

  let bool x =
    let module M = struct
      type a = bool

      module Interp (X:S) = struct
        let x = X.bool x
      end
    end in
    (module M : T with type a = bool)

  let (+) n p =
    let module M = struct
      type a = int

      module Interp (X:S) = struct
        let x =
          let module MN = (val n : T with type a=int) in
          let module IN = MN.Interp(X) in
          let n' = IN.x in
          let module MP = (val p : T with type a=int) in
          let module IP = MN.Interp(X) in
          let p' = IP.x in
          X.(n'+p')
      end
    end in
    (module M : T with type a = int)

  let if_ (type w) b (t:w t) (e:w t) =
    let module M = struct
      type a = w

      module Interp (X:S) = struct
        let x =
          let module MB = (val b : T with type a=bool) in
          let module IB = MB.Interp(X) in
          let b' = IB.x in
          let module MT = (val t : T with type a=w) in
          let module IT = MT.Interp(X) in
          let t' = IT.x in
          let module ME = (val e : T with type a=w) in
          let module IE = ME.Interp(X) in
          let e' = IE.x in
          X.if_ b' t' e'
      end
    end in
    (module M : T with type a = w)
end

My proposition of syntax aims at dealing gracefully with some of the
repetitive parts. It would look something like :

module Expr : sig
  include S

  val interp : (X:S) => 'a t -> 'a X.t
end = struct

  module type T = sig
    type a
    val interp : (X:S) => a X.t
  end

  type 'a t = (module T with type a = 'a)

  let interp {{X:S}} (type w) (e:w t) : w X.t =
    let module E = (val e : T with type a = w) in
    E.interp {{X}}

  let int x =
    let module M = struct
      type a = int
      let interp {{X:S}} = X.int x
    end in
    (module M : T with type a = int)

  let bool x =
    let module M = struct
      type a = bool
      let interp {{X:S}} = X.bool x
    end in
    (module M : T with type a = bool)

  let (+) n p =
    let module M = struct
      type a = int

      let interp {{X:S}} =
         let module MN = (val n : T with type a=int) in
         let module MP = (val p : T with type a=int) in
         X.((MN.interp {{X:S}})+(MP.interp {{X:S}})
      end
    end in
    (module M : T with type a = int)

  let if_ (type w) b (t:w t) (e:w t) =
    let module M = struct
      type a = w

      let interp {{X:S}} =
        let module MB = (val b : T with type a=bool) in
        let module MT = (val t : T with type a=w) in
        let module ME = (val e : T with type a=w) in
        X.if_ (MB.interp{{X:S}}) (MT.interp{{X:S}}) (ME.interp{{X:S}})
    end in
    (module M : T with type a = w)
end

The code could be shrinked even more dramatically if we were allowed to
define [Expr.t] directly as

type 'a t = (X:S) => 'a t

But I doubt it would be easy to make that possible. In my proposition, this
is the same as

type 'a t = (X:S) => 'b t

Which is unfortunate, but at least is quite compatible with how first-class
modules are dealt with in the current versions of OCaml.


--
Arnaud

--14dae9341141e4a7ef04c14192de
Content-Type: text/html; charset=UTF-8
Content-Transfer-Encoding: quoted-printable

Here is another kind of example I&#39;ve boiled down as much as I could (it=
 is somewhat related to the Leibniz equality).<br>Oleg Kiselyov and Jeremy =
Yallop ( <a href=3D"http://okmij.org/ftp/ML/first-class-modules/">http://ok=
mij.org/ftp/ML/first-class-modules/</a> ) have noticed that first-class mod=
ules could be leveraged to produce an variant of the Finally Tagless approa=
ch (which consist in replacing the use of a gadt by a typeclass signature, =
in Haskell, to denote expressions). I like to call it Initially Tagless.<br>

<br>The idea is to start with a signature representing your language, a fie=
ld for each language construct. Here, the language admits two types (int an=
d bool) and one operation on each:<br><br><div style=3D"margin-left:40px">

module type S =3D sig<br>=C2=A0 type &#39;a t<br><br>=C2=A0 val int : int -=
&gt; int t<br>=C2=A0 val bool : bool -&gt; bool t<br>=C2=A0 val (+) : int t=
 -&gt; int t -&gt; int t<br>=C2=A0 val if_ : bool t -&gt; &#39;a t -&gt; &#=
39;a t -&gt; &#39;a t<br>

end<br></div><br>An interpreter for the language is a module of type S. The=
 type of expressions [a Expr.t] is, then, defined as that of things which, =
for any interpretor X, can be interpreted into an [a X.t]. Here goes the co=
de in OCaml 3.12, you might notice it is very repetitive:<br>

<br><div style=3D"margin-left:40px">module Expr : sig<br>=C2=A0 include S<b=
r><br>=C2=A0 module Interp (X:S) : sig<br>=C2=A0=C2=A0=C2=A0 val x : &#39;a=
 t -&gt; &#39;a X.t<br>=C2=A0 end<br>end =3D struct<br><br>=C2=A0 module ty=
pe T =3D sig<br>=C2=A0=C2=A0=C2=A0 type a<br><br>=C2=A0=C2=A0=C2=A0 module =
Interp (X:S) : sig<br>

=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 val x : a X.t<br>=C2=A0=C2=A0=C2=A0 end<br>=
=C2=A0 end<br><br>=C2=A0 type &#39;a t =3D (module T with type a =3D &#39;a=
)<br><br>=C2=A0 module Interp (X:S) =3D struct<br>=C2=A0=C2=A0=C2=A0 let x =
(type w) (e:w t) : w X.t=3D<br>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 let module E =
=3D (val e : T with type a =3D w) in<br>

=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 let module IE =3D E.Interp(X) in<br>=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0 IE.x<br>=C2=A0 end<br><br>=C2=A0 let int x =3D<br>=
=C2=A0=C2=A0=C2=A0 let module M =3D struct<br>=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0 type a =3D int<br><br>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 module Interp (X:S=
) =3D struct<br>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 let x =3D X.int =
x<br>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 end<br>=C2=A0=C2=A0=C2=A0 end in<br>

=C2=A0=C2=A0=C2=A0 (module M : T with type a =3D int)<br><br>=C2=A0 let boo=
l x =3D<br>=C2=A0=C2=A0=C2=A0 let module M =3D struct<br>=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0 type a =3D bool<br><br>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 module I=
nterp (X:S) =3D struct<br>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 let x =
=3D X.bool x<br>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 end<br>=C2=A0=C2=A0=C2=A0 en=
d in<br>=C2=A0=C2=A0=C2=A0 (module M : T with type a =3D bool)<br>

<br>=C2=A0 let (+) n p =3D<br>=C2=A0=C2=A0=C2=A0 let module M =3D struct<br=
>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 type a =3D int<br><br>=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0 module Interp (X:S) =3D struct<br>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0 let x =3D<br>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0 let module MN =3D (val n : T with type a=3Dint) in<br>=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 let module IN =3D MN.Interp(X) i=
n<br>

=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 let n&#39; =3D IN.x =
in<br>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 let module MP =
=3D (val p : T with type a=3Dint) in<br>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0 let module IP =3D MN.Interp(X) in<br>=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 let p&#39; =3D IP.x in<br>=C2=A0=C2=
=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 X.(n&#39;+p&#39;)<br>=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0 end<br>=C2=A0=C2=A0=C2=A0 end in<br>

=C2=A0=C2=A0=C2=A0 (module M : T with type a =3D int)<br><br>=C2=A0 let if_=
 (type w) b (t:w t) (e:w t) =3D<br>=C2=A0=C2=A0=C2=A0 let module M =3D stru=
ct<br>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 type a =3D w<br><br>=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0 module Interp (X:S) =3D struct<br>=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0=C2=A0 let x =3D<br>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0 let module MB =3D (val b : T with type a=3Dbool) in<br>

=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 let module IB =3D MB=
.Interp(X) in<br>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 let=
 b&#39; =3D IB.x in<br>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0 let module MT =3D (val t : T with type a=3Dw) in<br>=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 let module IT =3D MT.Interp(X) in<br>=
=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 let t&#39; =3D IT.x =
in<br>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 let module ME =
=3D (val e : T with type a=3Dw) in<br>

=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 let module IE =3D ME=
.Interp(X) in<br>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 let=
 e&#39; =3D IE.x in<br>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0 X.if_ b&#39; t&#39; e&#39;<br>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 end<br>=C2=
=A0=C2=A0=C2=A0 end in<br>=C2=A0=C2=A0=C2=A0 (module M : T with type a =3D =
w)<br>end<br></div><br>My proposition of syntax aims at dealing gracefully =
with some of the repetitive parts. It would look something like :<br>

<br><div style=3D"margin-left:40px">module Expr : sig<br>=C2=A0 include S<b=
r><br>=C2=A0 val interp : (X:S) =3D&gt; &#39;a t -&gt; &#39;a X.t<br>end =
=3D struct<br><br>=C2=A0 module type T =3D sig<br>=C2=A0=C2=A0=C2=A0 type a=
<br>=C2=A0=C2=A0=C2=A0 val interp : (X:S) =3D&gt; a X.t<br>

=C2=A0 end<br><br>=C2=A0 type &#39;a t =3D (module T with type a =3D &#39;a=
)<br><br>=C2=A0 let interp {{X:S}} (type w) (e:w t) : w X.t =3D<br>=C2=A0=
=C2=A0=C2=A0 let module E =3D (val e : T with type a =3D w) in<br>=C2=A0=C2=
=A0=C2=A0 E.interp {{X}}<br><br>=C2=A0 let int x =3D<br>=C2=A0=C2=A0=C2=A0 =
let module M =3D struct<br>

=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 type a =3D int<br>=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0 let interp {{X:S}} =3D X.int x<br>=C2=A0=C2=A0=C2=A0 end in<br>=C2=
=A0=C2=A0=C2=A0 (module M : T with type a =3D int)<br><br>=C2=A0 let bool x=
 =3D<br>=C2=A0=C2=A0=C2=A0 let module M =3D struct<br>=C2=A0=C2=A0=C2=A0=C2=
=A0=C2=A0 type a =3D bool<br>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 let interp {{X:=
S}} =3D X.bool x<br>

=C2=A0=C2=A0=C2=A0 end in<br>=C2=A0=C2=A0=C2=A0 (module M : T with type a =
=3D bool)<br><br>=C2=A0 let (+) n p =3D<br>=C2=A0=C2=A0=C2=A0 let module M =
=3D struct<br>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 type a =3D int<br><br>=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0 let interp {{X:S}} =3D<br>=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0=C2=A0 let module MN =3D (val n : T with type a=3Dint) in=
<br>

=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 let module MP =3D (val p :=
 T with type a=3Dint) in<br>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0 X.((MN.interp {{X:S}})+(MP.interp {{X:S}})<br>=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0 end<br>=C2=A0=C2=A0=C2=A0 end in<br>=C2=A0=C2=A0=C2=A0 (module M : T=
 with type a =3D int)<br><br>=C2=A0 let if_ (type w) b (t:w t) (e:w t) =3D<=
br>

=C2=A0=C2=A0=C2=A0 let module M =3D struct<br>=C2=A0=C2=A0=C2=A0=C2=A0=C2=
=A0 type a =3D w<br><br>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 let interp {{X:S}} =
=3D<br>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 let module MB =3D (val b =
: T with type a=3Dbool) in<br>=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 le=
t module MT =3D (val t : T with type a=3Dw) in<br>=C2=A0=C2=A0=C2=A0=C2=A0=
=C2=A0=C2=A0=C2=A0 let module ME =3D (val e : T with type a=3Dw) in<br>

=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0=C2=A0 X.if_ (MB.interp{{X:S}}) (MT.int=
erp{{X:S}}) (ME.interp{{X:S}})<br>=C2=A0=C2=A0=C2=A0 end in<br>=C2=A0=C2=A0=
=C2=A0 (module M : T with type a =3D w)<br>end<br></div><br>The code could =
be shrinked even more dramatically if we were allowed to define [Expr.t] di=
rectly as<br>

<br><div style=3D"margin-left:40px">type &#39;a t =3D (X:S) =3D&gt; &#39;a =
t<br></div><br>But I doubt it would be easy to make that possible. In my pr=
oposition, this is the same as<br><br><div style=3D"margin-left:40px">type =
&#39;a t =3D (X:S) =3D&gt; &#39;b t<br>

</div><br>Which is unfortunate, but at least is quite compatible with how f=
irst-class modules are dealt with in the current versions of OCaml.<br><br>=
<br>--<br>Arnaud<br>

--14dae9341141e4a7ef04c14192de--