[Caml-list] How is this type inferred (GADTs)

[Malcolm Matalka <mmatalka@gmail.com>]

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