From: Malcolm Matalka <mmatalka@gmail.com> To: caml-list <caml-list@inria.fr> Subject: [Caml-list] How is this type inferred (GADTs) Date: Fri, 20 Sep 2019 11:42:29 +0800 Message-ID: <86o8zfpra2.fsf@gmail.com> (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) 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

next reply indexThread overview:6+ messages / expand[flat|nested] mbox.gz Atom feed top2019-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: https://en.wikipedia.org/wiki/Posting_style#Interleaved_style * Reply using the--to,--cc, and--in-reply-toswitches of git-send-email(1): git send-email \ --in-reply-to=86o8zfpra2.fsf@gmail.com \ --to=mmatalka@gmail.com \ --cc=caml-list@inria.fr \ /path/to/YOUR_REPLY https://kernel.org/pub/software/scm/git/docs/git-send-email.html * If your mail client supports setting theIn-Reply-Toheader via mailto: links, try the mailto: link

caml-list - the Caml user's mailing list Archives are clonable: git clone --mirror https://inbox.ocaml.org/caml-list AGPL code for this site: git clone https://public-inbox.org/ public-inbox