There is a direct relation between how type evolve du=
ring 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 Prolo=
g 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 pr=
ogramming 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 n=
ot done implicitly, as with type-class search for example), but it does giv=
e a way to think about GADT declarations.

Your dec=
laration (notice that I renamed 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

=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"))

| 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> 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)=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

>

> 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

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

>>