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 ESMTPS id 01C865D3 for ; Fri, 20 Sep 2019 08:11:38 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.64,527,1559512800"; d="scan'208";a="402630384" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 20 Sep 2019 10:11:37 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id CA5987EE31; Fri, 20 Sep 2019 10:11:37 +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 BE2947EE31 for ; Fri, 20 Sep 2019 10:11:34 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=mmatalka@gmail.com; spf=Pass smtp.mailfrom=mmatalka@gmail.com; spf=None smtp.helo=postmaster@mail-pg1-f193.google.com IronPort-PHdr: =?us-ascii?q?9a23=3ASxYQ1RTF9xtDV4pAFXz7fzrXMNpsv+yvbD5Q0YIu?= =?us-ascii?q?jvd0So/mwa6zZBWN2/xhgRfzUJnB7Loc0qyK6vumAzVLuMze+DBaKdoQDkVD0Z?= =?us-ascii?q?1X1yUbQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYn?= =?us-ascii?q?br+tQt2agMu4zf299IPOaAtUmjW9falyLBKrpgnNq8Uam4RvJrs/xxfTvHdEZu?= =?us-ascii?q?tayX52KV+Rgh3w4tu88IN5/ylfpv4t6dRMXbnmc6g9ULdVECkoP2cp6cPxqBLN?= =?us-ascii?q?VxGP5nwSUmUXlhpHHQ3I5wzkU5nyryX3qPNz1DGVMsPqQ780Xy+i77pwRx/zlC?= =?us-ascii?q?gHLT85/3rJhcF2kalWvQiupx17w47TfYGVKP9zdb7TcN8GWWZMWNtaWjdfCY2g?= =?us-ascii?q?cYQAE+sBPf5Zr4bjoVsOsQC+DhSoCO/21zNEmmP60ag83u88Ew/JwRYgEsoAsH?= =?us-ascii?q?varNv7KrocXuK7wqfLwjrMc+hb2Svh5IXSbhwtveuBUa52fMHMyUcvDQTFjlCI?= =?us-ascii?q?pILiJTyV0vgCs2+f7+plSOmhjHQoqx1rrTirxccjkJTCi4UQylDB7yp53Jw6Jd?= =?us-ascii?q?m7SEFhetOkH55QuDubN4tyWM8tX2ZouCMjx7AApJW1ci8KyJE9yB7ebfyKa4mI?= =?us-ascii?q?4hT5VOaQOzh0nnxleKinixaz90ig1uPxWteu3FdLsCVFiN7Mu3YQ3BLQ8siKUu?= =?us-ascii?q?Vx8lul1DqV1A3e6vtILV4pmafbMZIt37o9m5QLvUnCAyP6glv6gaGSe0k+++Wl?= =?us-ascii?q?6f7rbqjkq5OCMYJ/lxvwPb40msOlBOQ1KggOUHaf+eS7zLDj+Ff2QLROjvEviq?= =?us-ascii?q?nZv43WKd0VpqKkBwJY3Jwv6xm4Dzeh39QYmWcIIEhZdxKAiojlI1DOIPbmAvej?= =?us-ascii?q?m1mgjitnyvTcMrDiApjBNGbPnKrhcLpn9kJRzAQ+wcha551OC7EBJPzzWlX2tN?= =?us-ascii?q?zdFhI5Ngm0zPz7CNpn0oMeWniAD7SWMKPXq1CI5+YvL/OQa48SvTbxM+Il6OL2?= =?us-ascii?q?jX8lhV8derGk0ocNZ3C9GvRqOkGZYXv3gtcdCmoKpQo/TOnyiFKYSzJTZnCyX7?= =?us-ascii?q?g95j4hEo6mA53DFciRh+mu1S2hH5BSLltNCl2WHG2gI4qNUe0NZSbUOcRhnyYJ?= =?us-ascii?q?T5CuToYg0VelswqsmJR9Ke+B3yQcvpXn0ZBQ7vHakRI7vWhxCs2B2mWORkl7m2?= =?us-ascii?q?oJQ3k926Up8h818UuKzaUt268QLtdU/f4cF15ibceAndw/MMj7X0f6RvnMUEyv?= =?us-ascii?q?G4z0DjQ4T9Z3yNgLMR4kSoeSyyvb1i/vOIc70rmCBZg66KXZhiGjKMN0ynKA36?= =?us-ascii?q?4k3QB/H5l/cFa+j6s6zDD9Qo7El0LDyfSvfKUYmTbCrSKNlDvV+k5fVwF0XOPO?= =?us-ascii?q?WnVNPkY=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CtAQAbiYRddMHXVdFlHAEBAQQBAQcEA?= =?us-ascii?q?QGBZ4MFgRsUjR6IKJFXiUYJAQMBCgEBIwoCAQGEPwKDBxsHAQQ0EwIMAQEEAQE?= =?us-ascii?q?BAgECAwQBEwEKCwwHJ4U2DII6KQGCZgEBAQECARIVGQEbHQEDAQsGBQsNCSUPA?= =?us-ascii?q?RECEQEFARwGExsHgwGBaQEDDg4BD54/gQM8jCMWBQEXgn4FgUhBQIF1ChknDWI?= =?us-ascii?q?DgT0CBwkBCIEiimyBHRiBQD+DdS4+ghpHA4dDBJZEh16OKEFGgWaCLoRXigSEA?= =?us-ascii?q?RuDKIpFizeWLYIIjnoCCgcGDyOBRoF5MxoIGxU7MYI7CUcQFIFODBeDT4E+iSI?= =?us-ascii?q?zMwGBAiYTjXABAQ?= X-IPAS-Result: =?us-ascii?q?A0CtAQAbiYRddMHXVdFlHAEBAQQBAQcEAQGBZ4MFgRsUjR6?= =?us-ascii?q?IKJFXiUYJAQMBCgEBIwoCAQGEPwKDBxsHAQQ0EwIMAQEEAQEBAgECAwQBEwEKC?= =?us-ascii?q?wwHJ4U2DII6KQGCZgEBAQECARIVGQEbHQEDAQsGBQsNCSUPARECEQEFARwGExs?= =?us-ascii?q?HgwGBaQEDDg4BD54/gQM8jCMWBQEXgn4FgUhBQIF1ChknDWIDgT0CBwkBCIEii?= =?us-ascii?q?myBHRiBQD+DdS4+ghpHA4dDBJZEh16OKEFGgWaCLoRXigSEARuDKIpFizeWLYI?= =?us-ascii?q?IjnoCCgcGDyOBRoF5MxoIGxU7MYI7CUcQFIFODBeDT4E+iSIzMwGBAiYTjXABA?= =?us-ascii?q?Q?= X-IronPort-AV: E=Sophos;i="5.64,527,1559512800"; d="scan'208";a="402630378" X-MGA-submission: =?us-ascii?q?MDGXcjGeVRYMVxO/s+frssorFqqdwtqwely9EL?= =?us-ascii?q?5aG1rdFFi7QBMJHd5dXTGGyGg3m4ZtB2s4DpOMbb3Of/HwBotAQ74KkC?= =?us-ascii?q?bM6vRtQaiX4bMr2QnTtISRsWlBOP+o4S7N9CCrzwRQSUASxE688AqRlv?= =?us-ascii?q?GQF5N82rPUJvQ/78Qhk30J6Q=3D=3D?= Received: from mail-pg1-f193.google.com ([209.85.215.193]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 20 Sep 2019 10:11:33 +0200 Received: by mail-pg1-f193.google.com with SMTP id w10so3385198pgj.7 for ; Fri, 20 Sep 2019 01:11:33 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=references:user-agent:from:to:cc:subject:in-reply-to:date :message-id:mime-version; bh=7Aenh22aL32MM8oHTMR1x8taTS1Y1DkJQOj0OAPAZk0=; b=L7wjIxl66voIBhDIrlqD1rgXGGhPnB8MubW5lD0s4YuQl9PZO2zFgMw6W7wN+RTHcS 73SSjpikvfWHeWz6MfekwBv1/vlYZIQGJez8KblbhDhyVs/Hclip21hmTmDZgN7VKdjW siPBVRN3WkwUW+2e6kikhbuOA9WRZg12udum6gLpFdqLk/ShdYCdZm9ldaIqKwuTLblN 24yTJoeag714KxeNlEKiPOOBT6X9C9e8Svo1zzWGoe6K5Pnu9MY+h+j9QLI19NjJ2fdP BR5n5Cw+YIlz6hhbKMVO4BjAEFp6zN8pQpHZ/zOzPm3e2YU8d+pBcdBDADKhfrLanVRf sAwA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:references:user-agent:from:to:cc:subject :in-reply-to:date:message-id:mime-version; bh=7Aenh22aL32MM8oHTMR1x8taTS1Y1DkJQOj0OAPAZk0=; b=ARabSXVHKzL9sC09dd3ds0yTfcJg+yXzcPbvQrcsQwXmgPoxL9tDzxPsCXEsBcfboo t1b0MPx3td+7XAhtyy6X2T/fixGROdjk4Ku+6Rzh2748gIcBN9wt5xUDPSBzlXHvmN24 QtSFCi17YLpa+Wk7CCYHl5FCZivqhrkwIoiDqj110/oa4zoqmKQiCQ0TLNgBhUevn4ta NkqqQesSqZwDz0baRTk7fo/zrxyHKF9WS6fr81urxQ80H5DqBThDIQ+m47wxzKSvqorn mARMgpEdoDAJi3SXf27TXzGVjuxJPe2MJIPoCW6esUefNqD8HMRatetTv5sLMy4dD17J QS5Q== X-Gm-Message-State: APjAAAWAK0xYY8KeVFcJUHO48mdtFL00BPECK4pib6UnpDTXXg6plgWq T5h9Y+ljynjYS8u912pY5tnxizyussI= X-Google-Smtp-Source: APXvYqx9lAUIvSutSPFQhQGup0gkZNKPrw9H7SCkQA1firI+RRIi45ZLH3OPL8FRZ1+msuA3O5aUUQ== X-Received: by 2002:a65:6709:: with SMTP id u9mr14558580pgf.59.1568967091947; Fri, 20 Sep 2019 01:11:31 -0700 (PDT) Received: from localhost (061239067172.ctinets.com. [61.239.67.172]) by smtp.gmail.com with ESMTPSA id p66sm3236716pfg.127.2019.09.20.01.11.30 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Fri, 20 Sep 2019 01:11:30 -0700 (PDT) References: <86o8zfpra2.fsf@gmail.com> User-agent: mu4e 1.0; emacs 26.2 From: Malcolm Matalka To: Gabriel Scherer Cc: caml-list In-reply-to: Date: Fri, 20 Sep 2019 16:11:29 +0800 Message-ID: <86v9tnfkum.fsf@gmail.com> MIME-Version: 1.0 Content-Type: text/plain Subject: Re: [Caml-list] How is this type inferred (GADTs) Reply-To: Malcolm Matalka X-Loop: caml-list@inria.fr X-Sequence: 17814 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: 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 >>