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 D52D95D5 for ; Fri, 20 Sep 2019 14:23:43 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.64,528,1559512800"; d="scan'208";a="402711896" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 20 Sep 2019 16:23:38 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id E9A737EF5F; Fri, 20 Sep 2019 16:23:38 +0200 (CEST) Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id DD3D07EE31 for ; Fri, 20 Sep 2019 16:23:25 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=oleg@okmij.org; spf=Pass smtp.mailfrom=oleg@okmij.org; spf=None smtp.helo=postmaster@mail1.g3.pair.com IronPort-PHdr: =?us-ascii?q?9a23=3ARyDZLBc9T1A2lw1YPo/1UEISlGMj4u6mDksu8pMi?= =?us-ascii?q?zoh2WeGdxcu5bR7h7PlgxGXEQZ/co6odzbaP6Oa6Aydfvd7B6ClELMUWEUddyI?= =?us-ascii?q?0/pE8JOIa9E0r1LfrnPWQRPf9pcxtbxUy9KlVfA83kZlff8TWY5D8WHQjjZ0Iu?= =?us-ascii?q?frymUoHdgN6q2O+s5pbdfxtHhCanYbN1MR66sRjdutMZjId/JKs90AXFrmVHd+?= =?us-ascii?q?lUym5jOFafkwrh6suq85Nv7jpct+g9+8JcVKnxYrg1Q6FfADk6KW4++dfltQPE?= =?us-ascii?q?TQuB53scVnsZnx9VCAXb7x/0Q4n8vDLiuuVyxCeVM8v2TaspWTu59KdkVAXoiC?= =?us-ascii?q?YcODEn9mzcl9F9g7haoBKloBx/3pLUbYSIP/dwYq/RYdUXTndHU81MVSJOH5m8?= =?us-ascii?q?YpMBAeQBI+hWsorzqFQSohSjBwajCvjiyiNUinLswaE2z/4sHR/A0Qc9H9wOqn?= =?us-ascii?q?PUrNDtOakLVeC60qbIxijEYvNR3Tfy9ofIfwsmofGPWLJwcMjRxVMoFwPfgVWd?= =?us-ascii?q?sIroNC6b2OQKtmiU9etgVeS3hm4mrQFxvjaiytk2hojImI0V0FfE+CNky4g2Pd?= =?us-ascii?q?21UE92bN++HJZesyyWLYV7Ttk/T211tys20qMKtYKlcCQQ1pgr2hHSZ+aZf4WG?= =?us-ascii?q?/x7vTvudLSlmiH9jZbmxnQy98VK6xe35TsS00EhFri5CktTUs3ACzR3T6syaRv?= =?us-ascii?q?dn8Ues1yyD1xjJ5eFFO0A4j7bUK5kkwrIol5oTt1rMHjPulUj3jaKabEsp9+yy?= =?us-ascii?q?5+npeLnqu4KQOoBshgH7KKsum8i/AeoiMggJWmiW4eO81Ln98k32W7hKif42kq?= =?us-ascii?q?zYsJDYP8gbobS5AwBN3oY59xm/Fyum0MgfnXQfMF1KYheHj4zwN1HKIfD4Fuu/?= =?us-ascii?q?jk+3kDZrwvDGJqfuDo/MLnjFirfhfKxy51RSyAopnphj4MdRD7gdKfbwU2f+sd?= =?us-ascii?q?XZClkyNAnn7fzgDYBa0o4RETaIBqKWGKTRtF6KoOU1LL/fN8cupD/hJq19tLbV?= =?us-ascii?q?hngjlApFJPX77d4scHm9W89eDQCBe3O124UGEmILvEw5VuO40ATfAw4WXG67Wu?= =?us-ascii?q?cH3h9+CI+iCt6SFIWkgbjYmijgWIVfZ3oAAVeJQy+xJte0HswUYSfXGfdP1zkN?= =?us-ascii?q?VLyvUYgkjEj8swz/yrghKfDbqHQV?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0A3AAAy4IRdh3IDJ0JlGQEBAQEBAQEBA?= =?us-ascii?q?QEBAQcBAQEBAQGBZ4NeMo1IhhyCD5sdCQEDAQwtAgEBhD8CgwkbBwEENBMCDAE?= =?us-ascii?q?BBAEBAQIBAgMEARMBAQEKCwkIKYVAgjoigm8BAgIBJxM/BRYhNAWDfoF8DgGtG?= =?us-ascii?q?DOKS4E0jAkYgT9Ag3UuPoURgnCCJgSWRJZJgiyBeIohiGUnhDiUbqdZgWmBeU0?= =?us-ascii?q?wCDuCbU8QFIFojjoxAYE3jjkBAQ?= X-IPAS-Result: =?us-ascii?q?A0A3AAAy4IRdh3IDJ0JlGQEBAQEBAQEBAQEBAQcBAQEBAQG?= =?us-ascii?q?BZ4NeMo1IhhyCD5sdCQEDAQwtAgEBhD8CgwkbBwEENBMCDAEBBAEBAQIBAgMEA?= =?us-ascii?q?RMBAQEKCwkIKYVAgjoigm8BAgIBJxM/BRYhNAWDfoF8DgGtGDOKS4E0jAkYgT9?= =?us-ascii?q?Ag3UuPoURgnCCJgSWRJZJgiyBeIohiGUnhDiUbqdZgWmBeU0wCDuCbU8QFIFoj?= =?us-ascii?q?joxAYE3jjkBAQ?= X-IronPort-AV: E=Sophos;i="5.64,528,1559512800"; d="scan'208";a="320120507" X-MGA-submission: =?us-ascii?q?MDEOPqffathjaCysxzp2nq5Bh24yBuOdt9MMXD?= =?us-ascii?q?GlN2ebd0d9IXz72ZHQzJHwWgRvFWlYx4SSjR3V3sb8OcsUtZJZy2A3jj?= =?us-ascii?q?KSe8VUjSxqTzeVPnBrlT31MCTePtWL9Rn6YiCFMFvqp8S1EakHeOFyf0?= =?us-ascii?q?Nm2pBfKqd324Lt81MtmB668g=3D=3D?= Received: from mail1.g3.pair.com ([66.39.3.114]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 20 Sep 2019 16:23:23 +0200 Received: from mail1.g3.pair.com (localhost [127.0.0.1]) by mail1.g3.pair.com (Postfix) with ESMTP id 77E243FB1EC; Fri, 20 Sep 2019 10:23:21 -0400 (EDT) Received: from Melchior.localnet (122.231.214.202.rev.vmobile.jp [202.214.231.122]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by mail1.g3.pair.com (Postfix) with ESMTPSA id 54312582CAC; Fri, 20 Sep 2019 10:23:20 -0400 (EDT) Date: Fri, 20 Sep 2019 23:25:25 +0900 From: Oleg To: mmatalka@gmail.com Cc: caml-list@inria.fr Message-ID: <20190920142525.GA1829@Melchior.localnet> Mail-Followup-To: Oleg , mmatalka@gmail.com, caml-list@inria.fr MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <86o8zfpra2.fsf@gmail.com> User-Agent: Mutt/1.10.1 (2018-07-13) Subject: Re: [Caml-list] How is this type inferred (GADTs) Reply-To: Oleg X-Loop: caml-list@inria.fr X-Sequence: 17817 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 has given an excellent explanation, it is hard to add anything. Yet I will still try. > 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 Perhaps it will be easier to work out the types if we don't use GADTs. They are not necessary in your example (and not needed for the typed printf either). Here is the adjusted code module F : sig type ('f, 'r) t val z : ('r, 'r) t val (//) : ('f, 'a -> 'r) t -> (unit -> 'a) -> ('f, 'r) t val bind : 'f -> ('f, 'r) t -> 'r end = struct type ('f, 'r) t = 'f -> 'r let z = fun x -> x (* the type annotations are all optional. They are given to show which subexpressions have which types, and let the compiler confirm that. Alas, attaching type annotations requires too many parentheses *) let (//) : type a r f. (f, a -> r) t -> (unit -> a) -> (f, r) t = fun t th -> fun (f:f) -> ((((t f):(a->r)) (th () : a)) : r) let bind f t = t f end let exp1 = F.(z // (fun () -> Int32.zero) // (fun () -> ""));; (* val exp1 : (int32 -> string -> '_weak1, '_weak1) F.t = *) Just for reference, here is the implementation for the opposite order, suggested by Gabriel. module G : sig type ('f, 'r) t val z : ('r, 'r) t val (//) : ('f, 'r) t -> (unit -> 'a) -> ('a -> 'f, 'r) t val bind : 'f -> ('f, 'r) t -> 'r end = struct type ('f, 'r) t = {e: 'w. ('r -> 'w) -> ('f -> 'w)} let z = {e = fun x -> x} (* the type annotations are all optional. They are given to show which subexpressions have which types, and let the compiler confirm that Alas, attaching type annotations requires too many parentheses *) let (//) : type a r f. (f, r) t -> (unit -> a) -> (a->f, r) t = fun t th -> {e = fun (type w) (k:(r->w)) -> fun (af:a->f) -> ((((t.e k):(f -> w)) ((af (th ())):f)):w)} let bind f t = t.e (fun x -> x) f end let test = G.(z // (fun () -> 3l) // (fun () -> "foo"));; (* val test : (string -> int32 -> '_weak2, '_weak2) G.t = *) ;;