Note: the reason why you get _weak type variables (wh=
ich are not polymorphic, just not-inferred-yet)=C2=A0 is that the type-chec=
ker 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, an=
d 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 dire=
ctly, you would get slightly better types.

# S(S(Z=
, (fun () -> Int32.zero)), (fun () -> ""));;

- : (int32 = -> string -> 'a, 'a) t =3D S (S (Z, <fun>), <fun>= )

- : (int32 = -> string -> 'a, 'a) t =3D S (S (Z, <fun>), <fun>= )

Historically we have used module interfaces to i=
mplement "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 ho=
w the type-inference work (how variables are manipulated by the type-checke=
r and then "propagated back up"). This sounds like a difficult wa=
y to understand GADTs: you want to learn the typing rules *and* the type-in=
ference 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/d=
ocs/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 t=
ype and (2) any other valid type would be a specialization of this type, th=
ere is no simpler solution.

The second part: you w=
rote:

=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 bind (f (v ())) t

Let's f=
ocus on the second clause:

=C2=A0 =C2=A0 | S (=
t, v) ->

=C2=A0 =C2=A0 =C2=A0 bind (f (v ())) t

we kn=
ow 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:

=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 bind : type f r. f -> (f, r) t -> r

=C2=A0 f : (f,=
a -> r) t

=C2=A0 v : unit -> a

=C2=A0 expect=
ed return type: r

f does *not* have a function typ=
e here, so your idea of applying (f (v ())) cannot work (v does have a func=
tion type, so (v ()) is valid).

The only thing you=
can do on f is call (bind) recursively (with what arguments?), and then yo=
u will get an (a -> r) as result.

Do you see ho=
w to write a correct program from there?

=

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

<=
blockquote class=3D"gmail_quote" style=3D"margin:0px 0px 0px 0.8ex;border-l=
eft:1px solid rgb(204,204,204);padding-left:1ex">I have been using GADTs to=
make type-safe versions of APIs that are kindof like printf.=C2=A0 I've been using this pattern by rote and now I= 9;m

getting to trying to understand how it works.

I have the following code:

module F : sig

=C2=A0 type ('f, 'r) t

=C2=A0 val z : ('r, 'r) t

=C2=A0 val (//) : ('f, 'a -> 'r) t -> (unit -> 'a)= -> ('f, 'r) t

end =3D struct

=C2=A0 type ('f, 'r) t =3D

=C2=A0 =C2=A0 | Z : ('r, 'r) t

=C2=A0 =C2=A0 | S : (('f, 'a -> 'r) t * (unit -> 'a))= -> ('f, 'r) t

=C2=A0 let z =3D Z

=C2=A0 let (//) t f =3D S (t, f)

end

And the following usage:

utop # F.(z // (fun () -> Int32.zero) // (fun () -> ""));;<= br> - : (int32 -> string -> '_weak1, '_weak1) F.t =3D <abstr&g= t;

I understand how 'r is '_weak1 (I think), but I'm still trying = to figure

out how 'f gets its type by applying (//).=C2=A0 I think I have an

explanation below, and I'm hoping someone can say if it's correct a= nd/or

simplify it.

Explanation:

The constructor Z says that 'f and 'r, are the same (Z : ('r, &= #39;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).=C2=A0 And i= f

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 fo= r the

first application of (//) it makes sense.=C2=A0 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.=C2=A0 If the passed in (_, = _)

t must be (string -> '_weak), and the inner type actually must be (i= nt32

-> '_weak), then, the inner inner type must be ('_weak), the typ= e of 'r

at Z must be (string -> int32 -> '_weak), and since 'r, and &= #39;f are the

same type for Z, 'f must also be (string -> int32 -> '_weak),= and that

knowledge propagates back up?=C2=A0 But that doesn't feel quite right t= o 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:

=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 bind (f (v ())) t

However, this does not compile given:

Error: This expression has type f

=C2=A0 =C2=A0 =C2=A0 =C2=A0This 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.=C2=A0 A= nd

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 something.<= br>

Does this make sense?

What am I not understanding?

Thank you,

/Malcolm