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:
Archived-At:
List-Archive:
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
>>