caml-list - the Caml user's mailing list
 help / color / Atom feed
From: Gabriel Scherer <gabriel.scherer@gmail.com>
To: Malcolm Matalka <mmatalka@gmail.com>
Cc: caml-list <caml-list@inria.fr>
Subject: Re: [Caml-list] How is this type inferred (GADTs)
Date: Fri, 20 Sep 2019 10:35:06 +0200
Message-ID: <CAPFanBFAr5LOEXTdRJtrX6FUQ2_LVjbVgZqiZHLMyE6KkUPL8A@mail.gmail.com> (raw)
In-Reply-To: <86v9tnfkum.fsf@gmail.com>

[-- Attachment #1: Type: text/plain, Size: 9450 bytes --]

There is a direct relation between how type evolve during GADT typing and
how queries evolve during logic/relational programming. It can help to
think of a GADT declaration as the set of rules of a Prolog program. (I you
have never looked at Prolog, here is an occasion to learn something new).
That does *not* mean that GADTs let you do prolog-style programming in
types (the compiler will not automatically search for a proof, the user has
to write it down explicitly as a GADT term, so this work is not done
implicitly, as with type-class search for example), but it does give a way
to think about GADT declarations.

Your declaration (notice that I renamed the Z variable, for a good reason
that will appear clear below):

  type (_, _) t =
    | Z : ('f, 'f) t
    | S : (('f, 'a -> 'r) t * (unit -> 'a)) -> ('f, 'r) t

becomes

  t F F.
  t F R :- t F (A -> R), (unit -> A).

In any case, your declaration has the following effect:
- by the Z rule, all types of the form
  ('a1 -> 'a2 -> ... -> 'an -> 'r, 'a -> 'a2 -> ... -> 'an -> 'r) t
  are inhabited
- by the S rule, you can "hide" an element on the right
  (and you have to provide a thunk for it)
, moving from
  ('a1 -> ... -> 'an -> r, 'ak -> 'a{k+1} -> .. -> 'an -> r) t
  to
  ('a1 -> ... -> 'an -> r, 'a{k+1} -> .. -> 'an -> r) t

If you do this repeatedly you end up on what you want: ('a1 -> .. -> 'an ->
r, r) t.

The way you write about it, it sounds like you had the following
*different* definition in mind

type (_, _) t =
| Z : ('r, 'r) t
| S : ('f, 'r) t * (unit -> 'a) -> ('a -> 'f, 'r) t

let test = S (S (Z, (fun () -> 3l)), (fun () -> "foo"))

corresponding to the following Prolog program that I do find easier to
think about:

  t R R.
  t (A -> F) R :- t F R, (unit -> A).

It turns out that with this other definition, the first implementation that
you had written actually type-check fines.

(You could try to write conversion functions between those two definitions
to convince yourself that they are morally equivalent, but this is actually
a difficult exercise.)

On Fri, Sep 20, 2019 at 10:11 AM Malcolm Matalka <mmatalka@gmail.com> wrote:

>
> Gabriel Scherer <gabriel.scherer@gmail.com> writes:
>
> > Note: the reason why you get _weak type variables (which are not
> > polymorphic, just not-inferred-yet)  is that the type-checker cannot
> detect
> > that (z // (fun () -> ...)) is a value: it would have to unfold the call
> to
> > (//) for this, which it doesn't do in general, and here certainly could
> not
> > do given that its definition is hidden behind an abstraction boundary.
> > I would recommend experimenting *without* the module interface and the
> > auxiliary function, with the constructors directly, you would get
> slightly
> > better types.
> >
> > # S(S(Z, (fun () -> Int32.zero)), (fun () -> ""));;
> > - : (int32 -> string -> 'a, 'a) t = S (S (Z, <fun>), <fun>)
> >
> > Historically we have used module interfaces to implement "phantom types"
> --
> > because the type information there is only present in the interface, not
> in
> > the definition. With GADTs, the type constraints are built into the
> > definition itself, which is precisely what makes them more powerful; no
> > need for an abstract interface on top.
> >
> > The first part of your question is about understanding how the
> > type-inference work (how variables are manipulated by the type-checker
> and
> > then "propagated back up"). This sounds like a difficult way to
> understand
> > GADTs: you want to learn the typing rules *and* the type-inference
> > algorithm at once. But only the first part is necessary to use the
> feature
> > productively (with a few tips on when to use annotations, which are easy
> to
> > explain and in fact explained in the manual:
> > http://caml.inria.fr/pub/docs/manual-ocaml/manual033.html ). So instead
> of
> > asking: "how did the compiler get this type?", I would ask: "why is this
> > the right type"? I think you could convince yourself that (1) it is a
> > correct type and (2) any other valid type would be a specialization of
> this
> > type, there is no simpler solution.
> >
> > The second part: you wrote:
> >
> >   let rec bind : type f r. f -> (f, r) t -> r = fun f -> function
> >     | Z ->
> >       f
> >     | S (t, v) ->
> >       bind (f (v ())) t
> >
> > Let's focus on the second clause:
> >
> >     | S (t, v) ->
> >       bind (f (v ())) t
> >
> > we know that (f : f) holds, and that the pattern-matching is on a value
> of
> > type (f, r) t, and we must return r.
> > When pattern-matching on S (t, v), we learn extra type information from
> the
> > typing rule of S:
> >
> >     | S : (('f, 'a -> 'r) t * (unit -> 'a)) -> ('f, 'r) t
> >
> > if r has type (f, r) t, then (t, v) has type ((f, a -> r) t * (unit ->
> a))
> > for *some* unknown/existential type a. So within the branch we have
> >
> >   bind : type f r. f -> (f, r) t -> r
> >   f : (f, a -> r) t
> >   v : unit -> a
> >   expected return type: r
> >
> > f does *not* have a function type here, so your idea of applying (f (v
> ()))
> > cannot work (v does have a function type, so (v ()) is valid).
> >
> > The only thing you can do on f is call (bind) recursively (with what
> > arguments?), and then you will get an (a -> r) as result.
> >
> > Do you see how to write a correct program from there?
>
> Ah-ha!  I was close but my thinking was at the "wrong level" (I'm not
> sure how to put it).  The working implementation of bind is:
>
>   let rec bind : type f r. f -> (f, r) t -> r = fun f -> function
>     | Z ->
>       f
>     | S (t, v) ->
>       let f' = bind f t in
>       f' (v ())
>
> And now I see why you wanted me to look at it not through the module
> interface.  Looking at how the recursion would work, of course the
> most-nested S will have the function corresponding to the first
> parameter of the function.  I was thinking that I would consume the
> parameters on the way down, but it's actually on the way up.
>
> I am still working out in my head the answer to "why is this the right
> type", I think it has to slosh around in there a bit before it truly
> makes sense to me.
>
> Thank you!
>
> >
> >
> >
> > On Fri, Sep 20, 2019 at 5:42 AM Malcolm Matalka <mmatalka@gmail.com>
> wrote:
> >
> >> I have been using GADTs to make type-safe versions of APIs that are kind
> >> of like printf.  I've been using this pattern by rote and now I'm
> >> getting to trying to understand how it works.
> >>
> >> I have the following code:
> >>
> >> module F : sig
> >>   type ('f, 'r) t
> >>
> >>   val z : ('r, 'r) t
> >>   val (//) : ('f, 'a -> 'r) t -> (unit -> 'a) -> ('f, 'r) t
> >> end = struct
> >>   type ('f, 'r) t =
> >>     | Z : ('r, 'r) t
> >>     | S : (('f, 'a -> 'r) t * (unit -> 'a)) -> ('f, 'r) t
> >>
> >>   let z = Z
> >>   let (//) t f = S (t, f)
> >> end
> >>
> >> And the following usage:
> >>
> >> utop # F.(z // (fun () -> Int32.zero) // (fun () -> ""));;
> >> - : (int32 -> string -> '_weak1, '_weak1) F.t = <abstr>
> >>
> >> I understand how 'r is '_weak1 (I think), but I'm still trying to figure
> >> out how 'f gets its type by applying (//).  I think I have an
> >> explanation below, and I'm hoping someone can say if it's correct and/or
> >> simplify it.
> >>
> >> Explanation:
> >>
> >> The constructor Z says that 'f and 'r, are the same (Z : ('r, 'r) t).
> >> The constructor S says that the (_, _) t that it takes has some type 'f,
> >> but that the second type variable must be of the form 'a -> 'r, sort of
> >> deconstructing pattern match on the type (if that makes sense).  And if
> >> that (_, _) t is a Z, where we have stated the two type variables have
> >> the same value, that means 'f must also be ('a -> 'r). So for the
> >> first application of (//) it makes sense.  If we apply (//) again, the
> >> first parameter has the type (int32 -> '_weak1, '_weak1) t, but that
> >> must actually mean '_weak1 in this case is string -> '_weak, and then
> >> this is where things become jumbled in my head.  If the passed in (_, _)
> >> t must be (string -> '_weak), and the inner type actually must be (int32
> >> -> '_weak), then, the inner inner type must be ('_weak), the type of 'r
> >> at Z must be (string -> int32 -> '_weak), and since 'r, and 'f are the
> >> same type for Z, 'f must also be (string -> int32 -> '_weak), and that
> >> knowledge propagates back up?  But that doesn't feel quite right to me,
> >> either.
> >>
> >> With the help of reading other code, I've figured out how to make a
> >> function that uses a type like this that works like kprintf, however
> >> where I'm going in this case is that I want to take a function that
> >> matches 'f and apply it to the result of my functions.
> >>
> >> Something like:
> >>
> >>   let rec bind : type f r. f -> (f, r) t -> r = fun f -> function
> >>     | Z ->
> >>       f
> >>     | S (t, v) ->
> >>       bind (f (v ())) t
> >>
> >> However, this does not compile given:
> >>
> >> Error: This expression has type f
> >>        This is not a function; it cannot be applied.
> >>
> >> My understanding was if I have Z, and an input that has the type f, then
> >> that is just the return type since at Z, f and r are the same type.  And
> >> than at S, I can peel away the type of f by applying the function f and
> >> then recursively calling.  But my understanding is missing something.
> >>
> >> Does this make sense?
> >>
> >> What am I not understanding?
> >>
> >> Thank you,
> >> /Malcolm
> >>
>
>

[-- Attachment #2: Type: text/html, Size: 12567 bytes --]

<div dir="ltr"><div>There is a direct relation between how type evolve during GADT typing and how queries evolve during logic/relational programming. It can help to think of a GADT declaration as the set of rules of a Prolog program. (I you have never looked at Prolog, here is an occasion to learn something new). That does *not* mean that GADTs let you do prolog-style programming in types (the compiler will not automatically search for a proof, the user has to write it down explicitly as a GADT term, so this work is not done implicitly, as with type-class search for example), but it does give a way to think about GADT declarations.</div><div><br></div><div>Your declaration (notice that I renamed the Z variable, for a good reason that will appear clear below):<br></div><div><br></div><div>
  type (_, _) t =<br>
    | Z : (&#39;f, &#39;f) t<br>
    | S : ((&#39;f, &#39;a -&gt; &#39;r) t * (unit -&gt; &#39;a)) -&gt; (&#39;f, &#39;r) t</div><div><br></div><div>becomes<br></div><div><br></div><div>  t F F.<br></div><div>  t F R :- t F (A -&gt; R), (unit -&gt; A).</div><div><br></div><div>In any case, your declaration has the following effect:</div><div>- by the Z rule, all types of the form</div><div>  (&#39;a1 -&gt; &#39;a2 -&gt; ... -&gt; &#39;an -&gt; &#39;r, &#39;a -&gt; &#39;a2 -&gt; ... -&gt; &#39;an -&gt; &#39;r) t <br></div><div>  are inhabited<br></div><div>- by the S rule, you can &quot;hide&quot; an element on the right</div><div>  (and you have to provide a thunk for it)<br></div><div>, moving from</div><div>  (&#39;a1 -&gt; ... -&gt; &#39;an -&gt; r, &#39;ak -&gt; &#39;a{k+1} -&gt; .. -&gt; &#39;an -&gt; r) t<br></div><div>  to</div><div>  (&#39;a1 -&gt; ... -&gt; &#39;an -&gt; r, &#39;a{k+1} -&gt; .. -&gt; &#39;an -&gt; r) t<br><div>  <br></div><div>If you do this repeatedly you end up on what you want: (&#39;a1 -&gt; .. -&gt; &#39;an -&gt; r, r) t.</div><div><br></div><div>The way you write about it, it sounds like you had the following *different* definition in mind</div><div><br></div><div>type (_, _) t =<br>| Z : (&#39;r, &#39;r) t<br>| S : (&#39;f, &#39;r) t * (unit -&gt; &#39;a) -&gt; (&#39;a -&gt; &#39;f, &#39;r) t<br><br>let test = S (S (Z, (fun () -&gt; 3l)), (fun () -&gt; &quot;foo&quot;))</div><div><br></div><div>corresponding to the following Prolog program that I do find easier to think about:<br></div><div><br></div><div><div>  t R R.<br></div><div>  t (A -&gt; F) R :- t F R, (unit -&gt; A).</div><div><br></div></div><div>It turns out that with this other definition, the first implementation that you had written actually type-check fines.</div><div><br></div><div>(You could try to write conversion functions between those two definitions to convince yourself that they are morally equivalent, but this is actually a difficult exercise.)<br></div></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Fri, Sep 20, 2019 at 10:11 AM Malcolm Matalka &lt;<a href="mailto:mmatalka@gmail.com">mmatalka@gmail.com</a>&gt; wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><br>
Gabriel Scherer &lt;<a href="mailto:gabriel.scherer@gmail.com" target="_blank">gabriel.scherer@gmail.com</a>&gt; writes:<br>
<br>
&gt; Note: the reason why you get _weak type variables (which are not<br>
&gt; polymorphic, just not-inferred-yet)  is that the type-checker cannot detect<br>
&gt; that (z // (fun () -&gt; ...)) is a value: it would have to unfold the call to<br>
&gt; (//) for this, which it doesn&#39;t do in general, and here certainly could not<br>
&gt; do given that its definition is hidden behind an abstraction boundary.<br>
&gt; I would recommend experimenting *without* the module interface and the<br>
&gt; auxiliary function, with the constructors directly, you would get slightly<br>
&gt; better types.<br>
&gt;<br>
&gt; # S(S(Z, (fun () -&gt; Int32.zero)), (fun () -&gt; &quot;&quot;));;<br>
&gt; - : (int32 -&gt; string -&gt; &#39;a, &#39;a) t = S (S (Z, &lt;fun&gt;), &lt;fun&gt;)<br>
&gt;<br>
&gt; Historically we have used module interfaces to implement &quot;phantom types&quot; --<br>
&gt; because the type information there is only present in the interface, not in<br>
&gt; the definition. With GADTs, the type constraints are built into the<br>
&gt; definition itself, which is precisely what makes them more powerful; no<br>
&gt; need for an abstract interface on top.<br>
&gt;<br>
&gt; The first part of your question is about understanding how the<br>
&gt; type-inference work (how variables are manipulated by the type-checker and<br>
&gt; then &quot;propagated back up&quot;). This sounds like a difficult way to understand<br>
&gt; GADTs: you want to learn the typing rules *and* the type-inference<br>
&gt; algorithm at once. But only the first part is necessary to use the feature<br>
&gt; productively (with a few tips on when to use annotations, which are easy to<br>
&gt; explain and in fact explained in the manual:<br>
&gt; <a href="http://caml.inria.fr/pub/docs/manual-ocaml/manual033.html" rel="noreferrer" target="_blank">http://caml.inria.fr/pub/docs/manual-ocaml/manual033.html</a> ). So instead of<br>
&gt; asking: &quot;how did the compiler get this type?&quot;, I would ask: &quot;why is this<br>
&gt; the right type&quot;? I think you could convince yourself that (1) it is a<br>
&gt; correct type and (2) any other valid type would be a specialization of this<br>
&gt; type, there is no simpler solution.<br>
&gt;<br>
&gt; The second part: you wrote:<br>
&gt;<br>
&gt;   let rec bind : type f r. f -&gt; (f, r) t -&gt; r = fun f -&gt; function<br>
&gt;     | Z -&gt;<br>
&gt;       f<br>
&gt;     | S (t, v) -&gt;<br>
&gt;       bind (f (v ())) t<br>
&gt;<br>
&gt; Let&#39;s focus on the second clause:<br>
&gt;<br>
&gt;     | S (t, v) -&gt;<br>
&gt;       bind (f (v ())) t<br>
&gt;<br>
&gt; we know that (f : f) holds, and that the pattern-matching is on a value of<br>
&gt; type (f, r) t, and we must return r.<br>
&gt; When pattern-matching on S (t, v), we learn extra type information from the<br>
&gt; typing rule of S:<br>
&gt;<br>
&gt;     | S : ((&#39;f, &#39;a -&gt; &#39;r) t * (unit -&gt; &#39;a)) -&gt; (&#39;f, &#39;r) t<br>
&gt;<br>
&gt; if r has type (f, r) t, then (t, v) has type ((f, a -&gt; r) t * (unit -&gt; a))<br>
&gt; for *some* unknown/existential type a. So within the branch we have<br>
&gt;<br>
&gt;   bind : type f r. f -&gt; (f, r) t -&gt; r<br>
&gt;   f : (f, a -&gt; r) t<br>
&gt;   v : unit -&gt; a<br>
&gt;   expected return type: r<br>
&gt;<br>
&gt; f does *not* have a function type here, so your idea of applying (f (v ()))<br>
&gt; cannot work (v does have a function type, so (v ()) is valid).<br>
&gt;<br>
&gt; The only thing you can do on f is call (bind) recursively (with what<br>
&gt; arguments?), and then you will get an (a -&gt; r) as result.<br>
&gt;<br>
&gt; Do you see how to write a correct program from there?<br>
<br>
Ah-ha!  I was close but my thinking was at the &quot;wrong level&quot; (I&#39;m not<br>
sure how to put it).  The working implementation of bind is:<br>
<br>
  let rec bind : type f r. f -&gt; (f, r) t -&gt; r = fun f -&gt; function<br>
    | Z -&gt;<br>
      f<br>
    | S (t, v) -&gt;<br>
      let f&#39; = bind f t in<br>
      f&#39; (v ())<br>
<br>
And now I see why you wanted me to look at it not through the module<br>
interface.  Looking at how the recursion would work, of course the<br>
most-nested S will have the function corresponding to the first<br>
parameter of the function.  I was thinking that I would consume the<br>
parameters on the way down, but it&#39;s actually on the way up.<br>
<br>
I am still working out in my head the answer to &quot;why is this the right<br>
type&quot;, I think it has to slosh around in there a bit before it truly<br>
makes sense to me.<br>
<br>
Thank you!<br>
<br>
&gt;<br>
&gt;<br>
&gt;<br>
&gt; On Fri, Sep 20, 2019 at 5:42 AM Malcolm Matalka &lt;<a href="mailto:mmatalka@gmail.com" target="_blank">mmatalka@gmail.com</a>&gt; wrote:<br>
&gt;<br>
&gt;&gt; I have been using GADTs to make type-safe versions of APIs that are kind<br>
&gt;&gt; of like printf.  I&#39;ve been using this pattern by rote and now I&#39;m<br>
&gt;&gt; getting to trying to understand how it works.<br>
&gt;&gt;<br>
&gt;&gt; I have the following code:<br>
&gt;&gt;<br>
&gt;&gt; module F : sig<br>
&gt;&gt;   type (&#39;f, &#39;r) t<br>
&gt;&gt;<br>
&gt;&gt;   val z : (&#39;r, &#39;r) t<br>
&gt;&gt;   val (//) : (&#39;f, &#39;a -&gt; &#39;r) t -&gt; (unit -&gt; &#39;a) -&gt; (&#39;f, &#39;r) t<br>
&gt;&gt; end = struct<br>
&gt;&gt;   type (&#39;f, &#39;r) t =<br>
&gt;&gt;     | Z : (&#39;r, &#39;r) t<br>
&gt;&gt;     | S : ((&#39;f, &#39;a -&gt; &#39;r) t * (unit -&gt; &#39;a)) -&gt; (&#39;f, &#39;r) t<br>
&gt;&gt;<br>
&gt;&gt;   let z = Z<br>
&gt;&gt;   let (//) t f = S (t, f)<br>
&gt;&gt; end<br>
&gt;&gt;<br>
&gt;&gt; And the following usage:<br>
&gt;&gt;<br>
&gt;&gt; utop # F.(z // (fun () -&gt; Int32.zero) // (fun () -&gt; &quot;&quot;));;<br>
&gt;&gt; - : (int32 -&gt; string -&gt; &#39;_weak1, &#39;_weak1) F.t = &lt;abstr&gt;<br>
&gt;&gt;<br>
&gt;&gt; I understand how &#39;r is &#39;_weak1 (I think), but I&#39;m still trying to figure<br>
&gt;&gt; out how &#39;f gets its type by applying (//).  I think I have an<br>
&gt;&gt; explanation below, and I&#39;m hoping someone can say if it&#39;s correct and/or<br>
&gt;&gt; simplify it.<br>
&gt;&gt;<br>
&gt;&gt; Explanation:<br>
&gt;&gt;<br>
&gt;&gt; The constructor Z says that &#39;f and &#39;r, are the same (Z : (&#39;r, &#39;r) t).<br>
&gt;&gt; The constructor S says that the (_, _) t that it takes has some type &#39;f,<br>
&gt;&gt; but that the second type variable must be of the form &#39;a -&gt; &#39;r, sort of<br>
&gt;&gt; deconstructing pattern match on the type (if that makes sense).  And if<br>
&gt;&gt; that (_, _) t is a Z, where we have stated the two type variables have<br>
&gt;&gt; the same value, that means &#39;f must also be (&#39;a -&gt; &#39;r). So for the<br>
&gt;&gt; first application of (//) it makes sense.  If we apply (//) again, the<br>
&gt;&gt; first parameter has the type (int32 -&gt; &#39;_weak1, &#39;_weak1) t, but that<br>
&gt;&gt; must actually mean &#39;_weak1 in this case is string -&gt; &#39;_weak, and then<br>
&gt;&gt; this is where things become jumbled in my head.  If the passed in (_, _)<br>
&gt;&gt; t must be (string -&gt; &#39;_weak), and the inner type actually must be (int32<br>
&gt;&gt; -&gt; &#39;_weak), then, the inner inner type must be (&#39;_weak), the type of &#39;r<br>
&gt;&gt; at Z must be (string -&gt; int32 -&gt; &#39;_weak), and since &#39;r, and &#39;f are the<br>
&gt;&gt; same type for Z, &#39;f must also be (string -&gt; int32 -&gt; &#39;_weak), and that<br>
&gt;&gt; knowledge propagates back up?  But that doesn&#39;t feel quite right to me,<br>
&gt;&gt; either.<br>
&gt;&gt;<br>
&gt;&gt; With the help of reading other code, I&#39;ve figured out how to make a<br>
&gt;&gt; function that uses a type like this that works like kprintf, however<br>
&gt;&gt; where I&#39;m going in this case is that I want to take a function that<br>
&gt;&gt; matches &#39;f and apply it to the result of my functions.<br>
&gt;&gt;<br>
&gt;&gt; Something like:<br>
&gt;&gt;<br>
&gt;&gt;   let rec bind : type f r. f -&gt; (f, r) t -&gt; r = fun f -&gt; function<br>
&gt;&gt;     | Z -&gt;<br>
&gt;&gt;       f<br>
&gt;&gt;     | S (t, v) -&gt;<br>
&gt;&gt;       bind (f (v ())) t<br>
&gt;&gt;<br>
&gt;&gt; However, this does not compile given:<br>
&gt;&gt;<br>
&gt;&gt; Error: This expression has type f<br>
&gt;&gt;        This is not a function; it cannot be applied.<br>
&gt;&gt;<br>
&gt;&gt; My understanding was if I have Z, and an input that has the type f, then<br>
&gt;&gt; that is just the return type since at Z, f and r are the same type.  And<br>
&gt;&gt; than at S, I can peel away the type of f by applying the function f and<br>
&gt;&gt; then recursively calling.  But my understanding is missing something.<br>
&gt;&gt;<br>
&gt;&gt; Does this make sense?<br>
&gt;&gt;<br>
&gt;&gt; What am I not understanding?<br>
&gt;&gt;<br>
&gt;&gt; Thank you,<br>
&gt;&gt; /Malcolm<br>
&gt;&gt;<br>
<br>
</blockquote></div>

  reply index

Thread overview: 6+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2019-09-20  3:42 Malcolm Matalka
2019-09-20  6:35 ` Gabriel Scherer
2019-09-20  8:11   ` Malcolm Matalka
2019-09-20  8:35     ` Gabriel Scherer [this message]
2019-09-20  8:56       ` Gabriel Scherer
2019-09-20 14:25 ` Oleg

Reply instructions:

You may reply publically to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=CAPFanBFAr5LOEXTdRJtrX6FUQ2_LVjbVgZqiZHLMyE6KkUPL8A@mail.gmail.com \
    --to=gabriel.scherer@gmail.com \
    --cc=caml-list@inria.fr \
    --cc=mmatalka@gmail.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link

caml-list - the Caml user's mailing list

Archives are clonable:
	git clone --mirror http://inbox.vuxu.org/caml-list
	git clone --mirror https://inbox.ocaml.org/caml-list

Example config snippet for mirrors

Newsgroup available over NNTP:
	nntp://inbox.vuxu.org/vuxu.archive.caml-list


AGPL code for this site: git clone https://public-inbox.org/public-inbox.git