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 30DF45D3 for ; Fri, 20 Sep 2019 08:54:50 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.64,528,1559512800"; d="scan'208,217";a="402642730" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 20 Sep 2019 10:54:48 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id BE1927EF9F; Fri, 20 Sep 2019 10:54:48 +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 AB0F77EE31 for ; Fri, 20 Sep 2019 10:54:43 +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-qt1-f174.google.com IronPort-PHdr: =?us-ascii?q?9a23=3AVXvp4BYZglYQDMvwSJ8a3y7/LSx+4OfEezUN459i?= =?us-ascii?q?sYplN5qZr8W8bnLW6fgltlLVR4KTs6sC17ON9fq6EjReqdbZ6TZeKcYKD0dEwe?= =?us-ascii?q?wt3CUYSPafDkP6KPO4JwcbJ+9lEGFfwnegLEJOE9z/bVCB6le77DoVBwmtfVEt?= =?us-ascii?q?fre9FYHdldm42P6v8JPPfQpImCC9YbRvJxmqsAndrMYbjZZsJ6or1BfFvHREd/?= =?us-ascii?q?hXyGh1IV6fgwvw6t2/8ZJ+7Shcoe4t+9JFXa7nY6k2ULtUASg8PWso/sPrrx7D?= =?us-ascii?q?TQWO5nsYTGoblwdDDhbG4h/nQJr/qzP2ueVh1iaUO832Vq00Vi+576h3Uh/oiT?= =?us-ascii?q?wIOCA//WrKl8F/lqNboBampxxi347ZZZyeOfRicq/Be94RWHFMVdhNWSNfHoy8?= =?us-ascii?q?bpMPD+sfMuZes4n9vEYFoR+nCQWxGO/j1jpEi3nr1qM4zushCxnL0wMuH90MsH?= =?us-ascii?q?raotb7OroMX++p16TH1ynPYulM1Dvh9ITFcBYsquyMU7JqdsrRzFEiGQLfgVqL?= =?us-ascii?q?s4zlPi2a1uAQuGaG8+VgVfygi3Q5pAFrvzOiwcgshZPSiYIPy1DL6yF5zJwuJd?= =?us-ascii?q?KkSE50f8SkH4VKtyyBOIt2R9ktQ2BsuCog1rIGvpu7cTEMxZ86yRDfbPmHfJKJ?= =?us-ascii?q?4hLlTOuRIDF4hGhkeL2lnRqy/1KgxvX9VsmyzFZHoDRJnsPNt38TzRzT7c6KQe?= =?us-ascii?q?Z+8Ee5wTuDyRzf5+VeLU03lafXMYMtz78smpYJrEjOHCD7lUPrh6GMbEok4PKn?= =?us-ascii?q?6+H/b7XmuJCcM4h0hxn7Mqs0m8y/Bf00MhESX2SG4Oi82qDv8E/2TblQgf02la?= =?us-ascii?q?7ZsJ/eJcsFvKK2HwhV0oM75xa+CTepzsgYkGEZIF5ZfB+LlYvkNlHULPzlDPqz?= =?us-ascii?q?n06gnCppyv3JJrHhB4/CLnnHkLfvZ7Z97EtcxRI8zd9F/J1UELABL+z3WkPrr9?= =?us-ascii?q?zXEh85PBKuw+n5EtVwzYweWWeVDa+YNKPeq0OH5uUqI+WUfo8apC79K+Q55/7p?= =?us-ascii?q?lXI2hUUSfayt3ZcObHC4H+9mI1mCbHr3gtYBFH8KsRAkQOzrjl2CSz9TaGyoU6?= =?us-ascii?q?Iy/DFoQL6hWKLKQouqhLnJ+S6nF5lVbygSD1WFDX7sdIysVPIFaSbUKchkxG8q?= =?us-ascii?q?T7+kHqAo3wuvuQuy8LFnI/DZ4GVMupvpztl446vInhE/7zFuJ8uY2mCJCWpzmz?= =?us-ascii?q?VbFHcNwKljrBklmR+42q9ijqkdTIQLvq8bYkIBLZfZitdCJZXqQAuYJ4WGTV+n?= =?us-ascii?q?RpOtBjRjFotgke9LWF50HpCZtj6G2iOrB7EPkLnSXc4796vd2z76IMMvki+bhp?= =?us-ascii?q?lktEEvR450DUPjhqN78FKNVYvAkkHcjrrzMKpFg3KL+2CEwm6D+kpfVVwoXA?= =?us-ascii?q?=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BiCwCrkoRdgK6gVdFlHAEBAQQBAQcEA?= =?us-ascii?q?QGBZ4MFgQUWFIIGghyBHYJeixmCD5sdCQEDAQwjDAEBhD8CgwcbBwEENBMCDAE?= =?us-ascii?q?BBAEBAQIBAgMEARMBAQkNCQgnhTYMgjopAYJmAQEBAQIBEhEEGQEbFgcBAwELB?= =?us-ascii?q?gMCCwMKKgICIQEBEQEFARwGExsHgwABgWkBAw4PD489jwyBAzyLJH8WBQEXgn4?= =?us-ascii?q?FgUhBgjUKGScNYgOBPQIHEoEijAmBWD+BEYJkLj6CGkcDhGuCWASeIo17LUEHg?= =?us-ascii?q?iVlBIYciS9VhAEbgmVDlXyWLYIIjxMPI4EcKoF5MxojUDGCOwlHEBSBTgwXg0+?= =?us-ascii?q?BPokXQTABjysBAQ?= X-IPAS-Result: =?us-ascii?q?A0BiCwCrkoRdgK6gVdFlHAEBAQQBAQcEAQGBZ4MFgQUWFII?= =?us-ascii?q?GghyBHYJeixmCD5sdCQEDAQwjDAEBhD8CgwcbBwEENBMCDAEBBAEBAQIBAgMEA?= =?us-ascii?q?RMBAQkNCQgnhTYMgjopAYJmAQEBAQIBEhEEGQEbFgcBAwELBgMCCwMKKgICIQE?= =?us-ascii?q?BEQEFARwGExsHgwABgWkBAw4PD489jwyBAzyLJH8WBQEXgn4FgUhBgjUKGScNY?= =?us-ascii?q?gOBPQIHEoEijAmBWD+BEYJkLj6CGkcDhGuCWASeIo17LUEHgiVlBIYciS9VhAE?= =?us-ascii?q?bgmVDlXyWLYIIjxMPI4EcKoF5MxojUDGCOwlHEBSBTgwXg0+BPokXQTABjysBA?= =?us-ascii?q?Q?= X-IronPort-AV: E=Sophos;i="5.64,528,1559512800"; d="scan'208,217";a="402642712" X-MGA-submission: =?us-ascii?q?MDGGA2dqmemxI7nweE9b7ZMpGqWzO846+0pn3R?= =?us-ascii?q?GL80g7bKzOybLdwayayWYJ6UZHX9WSNg5OP/lryH+QXbXwjcKLU5t06w?= =?us-ascii?q?fwVY+cUYaC+oNBWkbdNtihZyCce3WLdmMf6yXg5bOR0KS+M+bNHu5Hbo?= =?us-ascii?q?q1U9c9fWMI+gbj1Tn6nD8IFA=3D=3D?= Received: from mail-qt1-f174.google.com ([209.85.160.174]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 20 Sep 2019 10:54:41 +0200 Received: by mail-qt1-f174.google.com with SMTP id w14so3350328qto.9 for ; Fri, 20 Sep 2019 01:54:41 -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=djzLj5uZljcpf491jYzFWGT1nw47M2OFFO+JqiMZGv8=; b=stkF1DdjaqsRaXIqyJz584c/UfjjeDOyHlvVkoK8duSA8BqOEQgt/KHOjS4iBLa0kH OGrXXDnudp5Tih1FOyvbaqRv+QOiTnkNpbp/TDabwDnzRzcPjMrEox6S/MURA0s3UVGM XJzIoiWyTKMVpj4FSwjYMqFgZkxB1wWUC1iUUdNAEhC0X+BBMSLd04O4ZgubiBtQpy/h wLFWWbuiIMf5lbuxmtvsNb6NG6LXBpMfAqL9kSovhKVOpy5GHpIqjV59XXFxz2CZ4yg/ BmVwzEwIpGHubj5JLzR82U5NcvJT09STy0JqLgPD4oNgi2nOzzqSEYPiiraC1236hrWP BFZA== 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=djzLj5uZljcpf491jYzFWGT1nw47M2OFFO+JqiMZGv8=; b=qH6YlK7Is5ePKlhFgzN1chlb95iE+pFohtykosvgllJ7+tBicGdwt8yfjJsudojlfz IZfA36RkNfot9RAtFGgBcEqMdEevAFi7cfTOs8lz57Ft9cgGQ1ZjJYiWWBStS+hvd0zL 4/icmm4v6Hp/Zd1fmv3FXCzby0gFeVXNlJ+ztUWvtd1f1BIBWfDoa7uMQE5Us5X5yZWV 6pYGW4L70nCy+ZHZNa1JqnLBLmcoWnN+NKRUqzuO2yd+9kQJsv8cVx0TV3NYGwbT52L4 VtEZO7r53UM11HZvRht5Zp/28RltIuCGp5LLggCI6mbZH3VOIL7ufQ99ZZnQd8eDpTHr sB0w== X-Gm-Message-State: APjAAAXJGlX19BMU3inpsoCzH/CurzuuWl7qGOqE61VoX8SyhrghHktE Dfn6eBNjjU0/npFYN4408CJwgMB09s4NWHGeVzC41Dacnqc= X-Google-Smtp-Source: APXvYqyGYhN9TdIAR7r6Q+7/Ce6CJCYzKSvny63YrkjSrjuS23RImPpnZXaFOHJkTBmztYg30JIfWMFle0ZmSRwMrkg= X-Received: by 2002:a0c:8749:: with SMTP id 9mr12178190qvi.174.1568969680442; Fri, 20 Sep 2019 01:54:40 -0700 (PDT) MIME-Version: 1.0 References: <86o8zfpra2.fsf@gmail.com> <86v9tnfkum.fsf@gmail.com> In-Reply-To: From: Gabriel Scherer Date: Fri, 20 Sep 2019 10:56:27 +0200 Message-ID: To: Malcolm Matalka Cc: caml-list Content-Type: multipart/alternative; boundary="0000000000007759870592f838cb" Subject: Re: [Caml-list] How is this type inferred (GADTs) Reply-To: Gabriel Scherer X-Loop: caml-list@inria.fr X-Sequence: 17816 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: --0000000000007759870592f838cb Content-Type: text/plain; charset="UTF-8" > (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.) type (_, _) t1 = | Z : ('f, 'f) t1 | S : (('f, 'a -> 'r) t1 * (unit -> 'a)) -> ('f, 'r) t1 type (_, _) t2 = | Z : ('r, 'r) t2 | S : ('f, 'r) t2 * (unit -> 'a) -> ('a -> 'f, 'r) t2 t2 is t1 "upside down" (and conversely). To go from t1 to t2 is thus a "reverse" operation. Just like for lists, writing "reverse" directly is difficult, but one can use an auxiliary function let rec rev_append : type a b c. (b, c) t2 -> (a, b) t1 -> (a, c) t2 On Fri, Sep 20, 2019 at 10:35 AM Gabriel Scherer wrote: > 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 >> >> >> >> --0000000000007759870592f838cb Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
> (You could try to write conversion functions bet= ween those two=20 definitions
> to convince yourself that they are morally equiv= alent,
> but=20 this is actually a difficult exercise.)

type (_, _= ) t1 =3D
| Z : ('f, 'f) t1
| S : (('f, 'a -> '= r) t1 * (unit -> 'a)) -> ('f, 'r) t1

type (_, _) t= 2 =3D
| Z : ('r, 'r) t2
| S : ('f, 'r) t2 * (unit -&g= t; 'a) -> ('a -> 'f, 'r) t2

<= div>t2 is t1 "upside down" (and conversely). To go from t1 to t2 = is thus a "reverse" operation.
Just like for lists, wri= ting "reverse" directly is difficult, but one can use an auxiliar= y function

let rec rev_append
=C2=A0 : type= a b c. (b, c) t2 -> (a, b) t1 -> (a, c) t2

=
= On Fri, Sep 20, 2019 at 10:35 AM Gabriel Scherer <gabriel.scherer@gmail.com> wrote:
There= is a direct relation between how type evolve during GADT typing and how qu= eries 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 neve= r 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 com= piler will not automatically search for a proof, the user has to write it d= own 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 ren= amed 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> wr= ote:

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

--0000000000007759870592f838cb--