> (You could try to write conversion functions bet= ween those two=20 definitions
> to convince yourself that they are morally equiv= alent,
> but=20 this is actually a difficult exercise.)

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

type (_, _) t= 2 =3D
| Z : ('r, 'r) t2
| S : ('f, 'r) t2 * (unit -&g= t; 'a) -> ('a -> 'f, 'r) t2

<= div>t2 is t1 "upside down" (and conversely). To go from t1 to t2 = is thus a "reverse" operation.
Just like for lists, wri= ting "reverse" directly is difficult, but one can use an auxiliar= y function

let rec rev_append
=C2=A0 : type= a b c. (b, c) t2 -> (a, b) t1 -> (a, c) t2

=
= On Fri, Sep 20, 2019 at 10:35 AM Gabriel Scherer <gabriel.scherer@gmail.com> wrote:
There= is a direct relation between how type evolve during GADT typing and how qu= eries 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 neve= r 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 com= piler will not automatically search for a proof, the user has to write it d= own 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 ren= amed the Z variable, for a good reason that will appear clear below):

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

becomes
=C2=A0 t F F.
=C2=A0 t F R :- t F (A -> R), (= unit -> A).

In any case, your declaration has t= he following effect:
- by the Z rule, all types of the form
=
=C2=A0 ('a1 -> 'a2 -> ... -> 'an -> 'r, &#= 39;a -> 'a2 -> ... -> 'an -> 'r) t
= =C2=A0 are inhabited
- by the S rule, you can "hide"= ; an element on the right
=C2=A0 (and you have to provide a thunk= for it)
, moving from
=C2=A0 ('a1 -> ... -&= gt; 'an -> r, 'ak -> 'a{k+1} -> .. -> 'an ->= r) t
=C2=A0 to
=C2=A0 ('a1 -> ... -> = 9;an -> r, 'a{k+1} -> .. -> 'an -> r) t
=C2=A0 =
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* defini= tion in mind

type (_, _) t =3D
| Z : ('r, &= #39;r) t
| S : ('f, 'r) t * (unit -> 'a) -> ('a -&= gt; 'f, 'r) t

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

corresponding to the f= ollowing Prolog program that I do find easier to think about:

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

It turns out that wit= h this other definition, the first implementation that you had written actu= ally type-check fines.

(You could try to write con= version functions between those two definitions to convince yourself that t= hey are morally equivalent, but this is actually a difficult exercise.)
=

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

Gabriel Scherer <gabriel.scherer@gmail.com> writes:

> Note: the reason why you get _weak type variables (which are not
> polymorphic, just not-inferred-yet)=C2=A0 is that the type-checker can= not 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 slig= htly
> better types.
>
> # S(S(Z, (fun () -> Int32.zero)), (fun () -> ""));; > - : (int32 -> string -> 'a, 'a) t =3D S (S (Z, <fun&g= t;), <fun>)
>
> Historically we have used module interfaces to implement "phantom= types" --
> because the type information there is only present in the interface, n= ot in
> the definition. With GADTs, the type constraints are built into the > definition itself, which is precisely what makes them more powerful; n= o
> 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 fea= ture
> productively (with a few tips on when to use annotations, which are ea= sy to
> explain and in fact explained in the manual:
> http://caml.inria.fr/pub/docs/manual-o= caml/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:
>
>=C2=A0 =C2=A0let rec bind : type f r. f -> (f, r) t -> r =3D fun = f -> function
>=C2=A0 =C2=A0 =C2=A0| Z ->
>=C2=A0 =C2=A0 =C2=A0 =C2=A0f
>=C2=A0 =C2=A0 =C2=A0| S (t, v) ->
>=C2=A0 =C2=A0 =C2=A0 =C2=A0bind (f (v ())) t
>
> Let's focus on the second clause:
>
>=C2=A0 =C2=A0 =C2=A0| S (t, v) ->
>=C2=A0 =C2=A0 =C2=A0 =C2=A0bind (f (v ())) t
>
> we know that (f : f) holds, and that the pattern-matching is on a valu= e of
> type (f, r) t, and we must return r.
> When pattern-matching on S (t, v), we learn extra type information fro= m the
> typing rule of S:
>
>=C2=A0 =C2=A0 =C2=A0| 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 >
>=C2=A0 =C2=A0bind : type f r. f -> (f, r) t -> r
>=C2=A0 =C2=A0f : (f, a -> r) t
>=C2=A0 =C2=A0v : unit -> a
>=C2=A0 =C2=A0expected 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!=C2=A0 I was close but my thinking was at the "wrong level"= (I'm not
sure how to put it).=C2=A0 The working implementation of bind is:

=C2=A0 let rec bind : type f r. f -> (f, r) t -> r =3D fun f -> fu= nction
=C2=A0 =C2=A0 | Z ->
=C2=A0 =C2=A0 =C2=A0 f
=C2=A0 =C2=A0 | S (t, v) ->
=C2=A0 =C2=A0 =C2=A0 let f' =3D bind f t in
=C2=A0 =C2=A0 =C2=A0 f' (v ())

And now I see why you wanted me to look at it not through the module
interface.=C2=A0 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.=C2=A0 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 ar= e kind
>> of like printf.=C2=A0 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
>>=C2=A0 =C2=A0type ('f, 'r) t
>>
>>=C2=A0 =C2=A0val z : ('r, 'r) t
>>=C2=A0 =C2=A0val (//) : ('f, 'a -> 'r) t -> (unit= -> 'a) -> ('f, 'r) t
>> end =3D struct
>>=C2=A0 =C2=A0type ('f, 'r) t =3D
>>=C2=A0 =C2=A0 =C2=A0| Z : ('r, 'r) t
>>=C2=A0 =C2=A0 =C2=A0| S : (('f, 'a -> 'r) t * (unit = -> 'a)) -> ('f, 'r) t
>>
>>=C2=A0 =C2=A0let z =3D Z
>>=C2=A0 =C2=A0let (//) t f =3D S (t, f)
>> end
>>
>> And the following usage:
>>
>> utop # F.(z // (fun () -> Int32.zero) // (fun () -> "&q= uot;));;
>> - : (int32 -> string -> '_weak1, '_weak1) F.t =3D &l= t;abstr>
>>
>> I understand how 'r is '_weak1 (I think), but I'm stil= l trying to figure
>> out how 'f gets its type by applying (//).=C2=A0 I think I hav= e 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 ty= pe '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).=C2= =A0 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.=C2=A0 If we apply (//) a= gain, 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.=C2=A0 If the passe= d in (_, _)
>> t must be (string -> '_weak), and the inner type actually m= ust 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 -> = 9;_weak), and that
>> knowledge propagates back up?=C2=A0 But that doesn't feel quit= e right to me,
>> either.
>>
>> With the help of reading other code, I've figured out how to m= ake a
>> function that uses a type like this that works like kprintf, howev= er
>> 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:
>>
>>=C2=A0 =C2=A0let rec bind : type f r. f -> (f, r) t -> r =3D = fun f -> function
>>=C2=A0 =C2=A0 =C2=A0| Z ->
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0f
>>=C2=A0 =C2=A0 =C2=A0| S (t, v) ->
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0bind (f (v ())) t
>>
>> However, this does not compile given:
>>
>> Error: This expression has type f
>>=C2=A0 =C2=A0 =C2=A0 =C2=A0 This is not a function; it cannot be ap= plied.
>>
>> 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= .=C2=A0 And
>> than at S, I can peel away the type of f by applying the function = f and
>> then recursively calling.=C2=A0 But my understanding is missing so= mething.
>>
>> Does this make sense?
>>
>> What am I not understanding?
>>
>> Thank you,
>> /Malcolm
>>

--0000000000007759870592f838cb--