From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by c5ff346549e7 (Postfix) with ESMTP id 3F3965D3 for ; Fri, 20 Sep 2019 08:33:40 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.64,528,1559512800"; d="scan'208,217";a="402636983" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 20 Sep 2019 10:33:35 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id F17EE7EF92; Fri, 20 Sep 2019 10:33:34 +0200 (CEST) Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 860E07EF0B for ; Fri, 20 Sep 2019 10:33:22 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gabriel.scherer@gmail.com; spf=Pass smtp.mailfrom=gabriel.scherer@gmail.com; spf=None smtp.helo=postmaster@mail-qk1-f175.google.com IronPort-PHdr: =?us-ascii?q?9a23=3ARC6BhxC0W/zKP75c7xh5UyQJP3N1i/DPJgcQr6Af?= =?us-ascii?q?oPdwSPTyocbcNUDSrc9gkEXOFd2Cra4d0KyM6eu4AyRAuc/H7ClYNsQUFlcsso?= =?us-ascii?q?Y/p0QYGsmLCEn2frbBThcRO4B8bmJj5GyxKkNPGczzNBX4q3y26iMOSF2kbVIm?= =?us-ascii?q?buv6FZTPgMupyuu854PcYxlShDq6fLh+MAi6oR/eu8ULj4ZuMLg9xgXGrndUZe?= =?us-ascii?q?hd2GdkKU6Okxrm6cq84YBv/z5Mt/498sJLTLn3cbk/QbFEFjotLno75NfstRnN?= =?us-ascii?q?TAuP4mUTX2ALmRdWAAbL8Q/3UI7pviT1quRy1i+aPdbrTb8vQjSt871rSB7zhy?= =?us-ascii?q?gZMTMy7XzahdZxjKJfpxKhugB/zovJa4ybKPZyYqXQds4BSGFfQsheSTBOAoKk?= =?us-ascii?q?b4sOEeUBO/pYr5LgrFcKtBeyGBWgCP/qxjJOm3T437A10/45HA7J0gwvHdIAvn?= =?us-ascii?q?rXotvoKqkdTfu4w7PUwTjZdf5axSvx5YrOfxs8of+MR7Vwcc/JxEcuDQzKlU+Q?= =?us-ascii?q?qY37MDORy+8DrnSU7+p+WuK1lWEnsRx6rz+gxsg2kYbJnIMVxU7A9Slj24Y6Od?= =?us-ascii?q?24R1BhYdG6CptdrC6aN45sTcMjR2Fkojo1yroDuZOieiUB1Zopxxnaa/OdcoiI?= =?us-ascii?q?5AruVOeXITdihXJqYqizhxio8US4y+38UNW03VhUoiZfk9jDqGoN1xvV58OaSf?= =?us-ascii?q?V95l+s1SiT2w3X8O1JIkA5mbDFJ5I/3LI8jIcfvEbDEyLwhU74lrWZdl8+9eit?= =?us-ascii?q?8+nnYqvpppubN4JsjwHxKKUumsimDeQhMQgCQnGX+eqh2LDh/UD1WrpKjvoxkq?= =?us-ascii?q?nWtJDVO94XqbK+Aw9Qyooj6hC/ACm60NkAg3ULMFZIdAiEgoXpIV3CPu70Aeml?= =?us-ascii?q?j1ixkjpmx+jKPrj7DZXMKnjDnq3hfbF460NExwo818tQ54hVCr4fJPL/QFTxu8?= =?us-ascii?q?DYDhAnKQy73fznBc5y1oMbQ22PA6uZPLnOvl+P4+IjO/OMa5MNuDbhN/gl4Obj?= =?us-ascii?q?gmMjll8YeamlxJ8XaHGjHvR6OEiZenrtgtIZEWgQpAY+TerqiEeDUTFJfXqyUb?= =?us-ascii?q?g8tXkHD9eDBIPIQYSoyJmIwC6/HZQeMmVDA0yFFXThX4qBUvYILimVJ5kyvCYD?= =?us-ascii?q?UO2OQoU71Byq/DTxy7d9I/CcriIRv4ji2dwz/ObTmAs/7xR7Cs2c1yeGSGQizT?= =?us-ascii?q?BAfCM/wK0q+R818VyEy6UtxqUATYUCtcMMaR8zMNvn98I/DtnzXgzbedLQEQSp?= =?us-ascii?q?R9ynBXc6SddjmoZSMXY4IM2ri1X45wTvG6UczuXZC5k986aa1H/0dZ4kliT2kZ?= =?us-ascii?q?I5hlxjefNhcG2rgqklqVrWDo/N1lyazuOkLPtBmiHK82iHwCyFu0QKCAM=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0AtCQCejYRdh6/eVdFlHAEBAQQBAQcEA?= =?us-ascii?q?QGBZ4MFgQUWFIIGghyBHYJeixqCD5sdCQEDAQwjDAEBhD8CgwcbBwEENBMCDAE?= =?us-ascii?q?BBAEBAQIBAgMEARMBAQEIDQkIKYU0DII6KQGCZgEBAQECARIRBBkBGxYHAQMBC?= =?us-ascii?q?wYDAgsDCioCAiEBAREBBQEcBhMIEweDAAGBaQEDDg8PjzGPDIEDPIskfxYFARe?= =?us-ascii?q?CfgWBSEGCNQoZJw1iA4E9AgcSgSKMCYFYP4ERgmQuPoIaRwOEa4JYBJ4ijXstQ?= =?us-ascii?q?QeCJWUEhhyJL1WEARuCZUOVfJYtggiPEw8jgRwqgXkzGiNQMYI7CUcQFIFODA4?= =?us-ascii?q?Jg0+BPokXQTABjysBAQ?= X-IPAS-Result: =?us-ascii?q?A0AtCQCejYRdh6/eVdFlHAEBAQQBAQcEAQGBZ4MFgQUWFII?= =?us-ascii?q?GghyBHYJeixqCD5sdCQEDAQwjDAEBhD8CgwcbBwEENBMCDAEBBAEBAQIBAgMEA?= =?us-ascii?q?RMBAQEIDQkIKYU0DII6KQGCZgEBAQECARIRBBkBGxYHAQMBCwYDAgsDCioCAiE?= =?us-ascii?q?BAREBBQEcBhMIEweDAAGBaQEDDg8PjzGPDIEDPIskfxYFAReCfgWBSEGCNQoZJ?= =?us-ascii?q?w1iA4E9AgcSgSKMCYFYP4ERgmQuPoIaRwOEa4JYBJ4ijXstQQeCJWUEhhyJL1W?= =?us-ascii?q?EARuCZUOVfJYtggiPEw8jgRwqgXkzGiNQMYI7CUcQFIFODA4Jg0+BPokXQTABj?= =?us-ascii?q?ysBAQ?= X-IronPort-AV: E=Sophos;i="5.64,528,1559512800"; d="scan'208,217";a="402636859" X-MGA-submission: =?us-ascii?q?MDFsq8dLiOOvadP2DKqvkejzgD/A93IfkeSbBQ?= =?us-ascii?q?ADxzJD50gYBviMOh+yFmOOHMEK4k+x+tRh/sN7aCOpBiVVwghn2bNPxb?= =?us-ascii?q?mByc0aqymnF6g6YzPB4pct+sniuSENpHXbAa039MtHuYgm/dJbpgx6oi?= =?us-ascii?q?Ti0owdDq7bunw9srsEf9Qnrw=3D=3D?= Received: from mail-qk1-f175.google.com ([209.85.222.175]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 20 Sep 2019 10:33:20 +0200 Received: by mail-qk1-f175.google.com with SMTP id f16so6475051qkl.9 for ; Fri, 20 Sep 2019 01:33:20 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:references:in-reply-to:from:date:message-id:subject:to :cc; bh=nNc5Kva7pO8oXC9cIwR4RrIk5KvQ0gFC54gmsGN4FVE=; b=YvwLrD0brV7p1wn5t0K0k5R+Iu1FJulELej8P/JQJ/czfFhkLOWIPDwCnJCX2/beWM AbIjeoKR0m/xE2JYcIGszS+8r0jblexbDV9GmTyPr86plTN5I2BLSESuugUapoH1H6X4 s5R2xJnR8B43egoOUnBzqVCCk7PwbW9796EHvIgoXNS6iAIVn/XcvboOW9hH2wBBaceY p6sto5Oac8xhRyfPIrRjD349Xi8EbaRfz+M1eWRO8ONYxxk4r3T4pUhvKrpxamSRN4AD XQ+PSybbUSYZDKSN5bVink0FZgaZJkuZ0k8IDRxobrpeQwqszq4GQM1fuNTr81qnO1BG 4d4g== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:references:in-reply-to:from:date :message-id:subject:to:cc; bh=nNc5Kva7pO8oXC9cIwR4RrIk5KvQ0gFC54gmsGN4FVE=; b=rzJs7bqwSbKaLcX7wQJUbIRHTqZ4OJg4Gvqrxo5gf9H1qpwFOR3JSyv1JAjQnOEuB6 14RFS7WlwjLhj6CZciY1l94dCs8rgyngrAWGZI5hygZfX0X52RbqNaKmThByvEwJ/CFJ pJwHbEZob5CRc8+qo58J3wKbMyERe10jRcUrQ8FhKvPBlmnBzYswZ05Y8gNI11SPCVzt y8ML2MdhIvdtEFwRnjjfs+5JDB92Ywh0N2WBLz+D9hK47E0ISVvqqKv8RkwxpLbPHgdX qb8rzyKHs9tgASDUQJocquKDLfjhNCvr/ICYkOb6Wgs2MMVqScL3nYP9dYDAXnPwTkjr k30w== X-Gm-Message-State: APjAAAX/3L8RjzZ7YIWWB/ZfX+y+VTzwyD4G8yIhjqjIzUHnui8Zr9Uc PKDbRNDo7F0wYJ5LtLAX2ZUefv/+khj85SdoG6rEOLvTIiY= X-Google-Smtp-Source: APXvYqzOmM0hEJWh6WLyO8x2D+vw134aOLHu3ng5Lun4ufMfkrpBjLjpgbV8PK6FJ9BULUu+J+DTpFgywlyn0mVRiHs= X-Received: by 2002:a05:620a:40f:: with SMTP id 15mr2510396qkp.274.1568968399081; Fri, 20 Sep 2019 01:33:19 -0700 (PDT) MIME-Version: 1.0 References: <86o8zfpra2.fsf@gmail.com> <86v9tnfkum.fsf@gmail.com> In-Reply-To: <86v9tnfkum.fsf@gmail.com> From: Gabriel Scherer Date: Fri, 20 Sep 2019 10:35:06 +0200 Message-ID: To: Malcolm Matalka Cc: caml-list Content-Type: multipart/alternative; boundary="00000000000017576b0592f7ecea" Subject: Re: [Caml-list] How is this type inferred (GADTs) Reply-To: Gabriel Scherer X-Loop: caml-list@inria.fr X-Sequence: 17815 Errors-to: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: --00000000000017576b0592f7ecea Content-Type: text/plain; charset="UTF-8" There is a direct relation between how type evolve during 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 Prolog 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 programming 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 not done implicitly, as with type-class search for example), but it does give a way to think about GADT declarations. Your declaration (notice that I renamed the Z variable, for a good reason that will appear clear below): type (_, _) t = | Z : ('f, 'f) t | S : (('f, 'a -> 'r) t * (unit -> 'a)) -> ('f, 'r) t becomes t F F. t F R :- t F (A -> R), (unit -> A). In any case, your declaration has the following effect: - by the Z rule, all types of the form ('a1 -> 'a2 -> ... -> 'an -> 'r, 'a -> 'a2 -> ... -> 'an -> 'r) t are inhabited - by the S rule, you can "hide" an element on the right (and you have to provide a thunk for it) , moving from ('a1 -> ... -> 'an -> r, 'ak -> 'a{k+1} -> .. -> 'an -> r) t to ('a1 -> ... -> 'an -> r, 'a{k+1} -> .. -> 'an -> r) t 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* definition in mind type (_, _) t = | Z : ('r, 'r) t | S : ('f, 'r) t * (unit -> 'a) -> ('a -> 'f, 'r) t let test = S (S (Z, (fun () -> 3l)), (fun () -> "foo")) corresponding to the following Prolog program that I do find easier to think about: t R R. t (A -> F) R :- t F R, (unit -> A). It turns out that with this other definition, the first implementation that you had written actually type-check fines. (You could try to write conversion functions between those two definitions to convince yourself that they are morally equivalent, but this is actually a difficult exercise.) On Fri, Sep 20, 2019 at 10:11 AM Malcolm Matalka wrote: > > Gabriel Scherer writes: > > > Note: the reason why you get _weak type variables (which are not > > polymorphic, just not-inferred-yet) is that the type-checker 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, 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 > slightly > > better types. > > > > # S(S(Z, (fun () -> Int32.zero)), (fun () -> ""));; > > - : (int32 -> string -> 'a, 'a) t = S (S (Z, ), ) > > > > Historically we have used module interfaces to implement "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 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 > 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/docs/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 type and (2) any other valid type would be a specialization of > this > > type, there is no simpler solution. > > > > The second part: you wrote: > > > > let rec bind : type f r. f -> (f, r) t -> r = fun f -> function > > | Z -> > > f > > | S (t, v) -> > > bind (f (v ())) t > > > > Let's focus on the second clause: > > > > | S (t, v) -> > > bind (f (v ())) t > > > > we know 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: > > > > | 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 > > > > bind : type f r. f -> (f, r) t -> r > > f : (f, a -> r) t > > v : unit -> a > > expected 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 > > arguments?), and then you will get an (a -> r) as result. > > > > Do you see how to write a correct program from there? > > Ah-ha! I was close but my thinking was at the "wrong level" (I'm not > sure how to put it). The working implementation of bind is: > > let rec bind : type f r. f -> (f, r) t -> r = fun f -> function > | Z -> > f > | S (t, v) -> > let f' = bind f t in > f' (v ()) > > And now I see why you wanted me to look at it not through the module > interface. 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. 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 > makes sense to me. > > Thank you! > > > > > > > > > On Fri, Sep 20, 2019 at 5:42 AM Malcolm Matalka > wrote: > > > >> 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 = > >> > >> 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 > >> > > --00000000000017576b0592f7ecea Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
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

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

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 > arguments?), and then you will get an (a -> r) as result.
>
> 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 makes sense to me.

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

--00000000000017576b0592f7ecea--