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 9B7195D4 for ; Fri, 20 Sep 2019 03:42:44 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.64,527,1559512800"; d="scan'208";a="402593811" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 20 Sep 2019 05:42:43 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id 82E5B7EF3A; Fri, 20 Sep 2019 05:42:43 +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 6EA667EF3A for ; Fri, 20 Sep 2019 05:42:35 +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-pl1-f170.google.com IronPort-PHdr: =?us-ascii?q?9a23=3AwI1e7hz7y8WnWOPXCy+O+j09IxM/srCxBDY+r6Qd?= =?us-ascii?q?2+gUIJqq85mqBkHD//Il1AaPAdyAragdwLWM++C4ACpcuMzH6ChDOLV3FDY9wf?= =?us-ascii?q?0MmAIhBMPXQWbaF9XNKxIAIcJZSVV+9Gu6O0UGUOz3ZlnVv2HgpWVKQka3OgV6?= =?us-ascii?q?PPn6FZDPhMqrye+y54fTYwJVjzahfL9+Nhq7oRjfu8UMn4duN6k9xxnXrnBVf+?= =?us-ascii?q?ha2X5kKUickhrh+Mu85oJv/zhVt/k868NOTKL2crgiQ7dFFjomKWc15MPqtRnH?= =?us-ascii?q?UwSC42YXX3sVnBRVHQXL9Qn2UZjtvCT0sOp9wzSaMtbtTb8oQzSi7rxkRwHuhS?= =?us-ascii?q?waKjM26mDXish3jKJGvBKsogF0zoDIbI2JMvd1Y6XQds4YS2VcRMZcTyJODIOi?= =?us-ascii?q?YYUSAeQPPulXoJXmqlsSsRezHxWgCP/1xzNUgHL9wK000/4mEQHDxAEuGMgBsH?= =?us-ascii?q?DIo9XyMKcSVP2+wq7SwjXfdfxW3TT955LVeR0mpPGMWKh/cdbLxkkrFAPKlE6d?= =?us-ascii?q?qYPgPzyP1+QNt3KX4PZnVeKqkmMqrRx6rDaoxscpkIbJh4QVx0jF9SV/3IY4K8?= =?us-ascii?q?O0RFR6YNG6CptQsCeXPJZ1TMM6W2xkpjo2x7kctZO4fCUG0oorywPQZvCdboSF?= =?us-ascii?q?4A7vWP6QLDtlnn5pZryyihKo/UWhyODwTNS43VRUoidDj9LCrGoC1wbJ5ciCUv?= =?us-ascii?q?Z9/lmu2TKI1w3L7+FLO0E0la7CJ545xr48i4MfsUreEiL0hEn6lqCWdkIj+uin?= =?us-ascii?q?7+TofK/qqYObN49xkg3+M6IuldKjAekgLAQCQ2yW9f6/2bDj50H1XqhGg/Isnq?= =?us-ascii?q?XEsp3WOdwXpqujDA9U1oYj5Qy/DzCj0NkAmHkHKUhKeA6dgIjtOFHBOuv1Dfi6?= =?us-ascii?q?g1u2kTdrw+rKMaHmApXINnTDiqvufa5h605Azwo+1cxQ6IhRCrEFOf7zXk7xtM?= =?us-ascii?q?fEDhIiKAy1w+PnCM1n2Y8EWGKPBLWZMKLIvlOS6OIvObrEWIhAsz/4L70h5uXy?= =?us-ascii?q?xSsykFoZOK2oxoc/aXaiH/0gLV/PMlT2hdJUNG4OtQ06SaTPgUGLVT1aLyK3Wq?= =?us-ascii?q?sg7zU4AaqpCI7CQsamh7nXj3TzJYFfem0TUgPEKnzvbYjRA65dOhLXGddol3k/?= =?us-ascii?q?bZbkToYg0R+0swqjkuhoK+PV/msTspexjYEotd2Wrgk78HlPN+rY02yJSDsqzG?= =?us-ascii?q?YBRjtzxKQm5EIklQ/F3q9/jPhVU9dU4qERC1toBdvn1+V/TuvKdEfZZN7QEQSp?= =?us-ascii?q?R9ynBXc6Sddjm9I=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BGCAC2SYRdh6rWVdFmghmENI0ehhiMB?= =?us-ascii?q?3SGa4lGCQEDAQoBAQUoAgEBh0QbBwEEMwYOAgwBAQQBAQECAQIDBAETAQEBCA0?= =?us-ascii?q?JCCmFNAyCOiKDBxUZARseAxIQFjQBExEBBQEiNYMAgWoBAxwBnluBAzyMIxYFA?= =?us-ascii?q?ReCfgWCSYF2ChknDWIDgT0CBwkBCIEijAkYgUA/jwgElkSWR0aBZgOCK5JcG41?= =?us-ascii?q?tizenLwIKBwYPI4FFgXozGggbFWyCO1AQFIFog1iKYDMzgQMmE41wAQE?= X-IPAS-Result: =?us-ascii?q?A0BGCAC2SYRdh6rWVdFmghmENI0ehhiMB3SGa4lGCQEDAQo?= =?us-ascii?q?BAQUoAgEBh0QbBwEEMwYOAgwBAQQBAQECAQIDBAETAQEBCA0JCCmFNAyCOiKDB?= =?us-ascii?q?xUZARseAxIQFjQBExEBBQEiNYMAgWoBAxwBnluBAzyMIxYFAReCfgWCSYF2Chk?= =?us-ascii?q?nDWIDgT0CBwkBCIEijAkYgUA/jwgElkSWR0aBZgOCK5JcG41tizenLwIKBwYPI?= =?us-ascii?q?4FFgXozGggbFWyCO1AQFIFog1iKYDMzgQMmE41wAQE?= X-IronPort-AV: E=Sophos;i="5.64,527,1559512800"; d="scan'208";a="402593804" X-MGA-submission: =?us-ascii?q?MDHR9jDGQvaoPWzpQY6O9zkW0se57H3ns1PMuV?= =?us-ascii?q?cVdjrM8aHehFGzWVhR3ZA2c9usg4HZn0JKhz5cdjXmmHa/mPL+XtRwmn?= =?us-ascii?q?0a5jKUzRWGRTKcNoBdwNkSM0A39Nm2lbklOUdNYSVGxTGU9GKsErf7Z1?= =?us-ascii?q?0VPfs3tlkx5WeUO4sr1tDx1g=3D=3D?= Received: from mail-pl1-f170.google.com ([209.85.214.170]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 20 Sep 2019 05:42:34 +0200 Received: by mail-pl1-f170.google.com with SMTP id u12so2534775pls.12 for ; Thu, 19 Sep 2019 20:42:34 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=user-agent:from:to:subject:date:message-id:mime-version; bh=a6RVk5SN1awL2mAfjD2VymrFonbTAKc41hTubuFJYmk=; b=faDT1J2ffdT0N7YU1+z3hppbPZMcNb/+22U2GvIb0PuByNnXRlKZsY1tXqCPM7YmX9 kpWIFYWWwZYveIxLzwiFlxBLD9w3N/EQThoDOg8uBlKm6Z5qLJW7UMTTg61wAngzIRJC Qe66G1Y7j8B5owbQTS1wDXSWH2TcC5jQM2CU8Qp+AEwHaeJQFPypioWo6HxA40576riK PV+Olbw2mg861o0pNIdH/ak1pysMSFupBkOthdio9W1sX1X4Mjcy2694QdlOERyP7x99 tTf3ZCN9gH6EsRz1qISJfUUaooZdLYruDfLR43NjMfpdoNpCnQhTLp/YSGlkx3xCOwAf oWgg== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:user-agent:from:to:subject:date:message-id :mime-version; bh=a6RVk5SN1awL2mAfjD2VymrFonbTAKc41hTubuFJYmk=; b=hZcDM+WJDiRjjJkac1t79jEs/h/4qy3D2T7ctAfnVYZx515MQqNK4GmiODkA2oGzQe orSk0n88i8+Db6V6LzII2x/pYuzYHShf+KKDuJTKNM3pXY6InS518XIZrX4mLS2EBrr9 RtkZTmnZ7zDA91iQ4HB2MXL8qNoL/pnmnu7i7Nm4YPi3q5oQfbt/wzRM2oNOUvrAMEj0 mnvhL/XybgjwNs8/e85HJG6PbUv6nNZd0Wdiu1h2qD5vT/4fSABqvhv9VK9xYeLJsv+E Yq3x6X8CfX3F8vxthcjSmccAGxdT0mqjWcEWv8V6Tn/nF1PrpLiZf+q93CdDnWomIiJc FjZg== X-Gm-Message-State: APjAAAVDqnF9cmZ69H8VwLCm4uUbrXg7vw+HX/r/oSZfrwXbQHrNxwIF AfNVSWbcn/2qaSGDqe+VREO3Pz9JUbA= X-Google-Smtp-Source: APXvYqxAg3UWcJOF5qZCJCHcxvzjpGNm2RH4d5PYyp6phSQb5hgrqoUdy1QepBLZNtRTTUMUUHRlOQ== X-Received: by 2002:a17:902:7c89:: with SMTP id y9mr13784619pll.115.1568950952386; Thu, 19 Sep 2019 20:42:32 -0700 (PDT) Received: from localhost (061239067172.ctinets.com. [61.239.67.172]) by smtp.gmail.com with ESMTPSA id n66sm543299pfn.90.2019.09.19.20.42.30 for (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Thu, 19 Sep 2019 20:42:31 -0700 (PDT) User-agent: mu4e 1.0; emacs 26.2 From: Malcolm Matalka To: caml-list Date: Fri, 20 Sep 2019 11:42:29 +0800 Message-ID: <86o8zfpra2.fsf@gmail.com> MIME-Version: 1.0 Content-Type: text/plain Subject: [Caml-list] How is this type inferred (GADTs) Reply-To: Malcolm Matalka X-Loop: caml-list@inria.fr X-Sequence: 17812 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: 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