caml-list - the Caml user's mailing list
 help / Atom feed
From: Malcolm Matalka <>
To: caml-list <>
Subject: [Caml-list] How is this type inferred (GADTs)
Date: Fri, 20 Sep 2019 11:42:29 +0800
Message-ID: <> (raw)

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)

And the following usage:

utop # F.(z // (fun () -> // (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.


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,

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 ->
    | 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,

             reply index

Thread overview: 6+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2019-09-20  3:42 Malcolm Matalka [this message]
2019-09-20  6:33 ` Gabriel Scherer
2019-09-20  8:11   ` Malcolm Matalka
2019-09-20  8:33     ` Gabriel Scherer
2019-09-20  8:54       ` Gabriel Scherer
2019-09-20 14:23 ` 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:

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

  git send-email \ \ \ \

* 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

AGPL code for this site: git clone public-inbox