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 BA2BE5D5 for ; Tue, 7 Jan 2020 19:25:05 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.69,407,1571695200"; d="scan'208";a="430297511" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 07 Jan 2020 20:25:04 +0100 Received: by sympa.inria.fr (Postfix, from userid 20132) id 5F6477F3CE; Tue, 7 Jan 2020 20:25:04 +0100 (CET) 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 D0EA87F214 for ; Tue, 7 Jan 2020 20:25:00 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=rixed@happyleptic.org; spf=Pass smtp.mailfrom=rixed@happyleptic.org; spf=Pass smtp.helo=postmaster@wout1-smtp.messagingengine.com IronPort-PHdr: =?us-ascii?q?9a23=3ARvbDGhJXL3GFTLnn2NmcpTZWNBhigK39O0sv0rFi?= =?us-ascii?q?tYgRK/7xwZ3uMQTl6Ol3ixeRBMOHsqkC0beI+Pi+EUU7or+5+EgYd5JNUxJXwe?= =?us-ascii?q?43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRp?= =?us-ascii?q?OOv1BpTSj8Oq3Oyu5pHfeQpFiCezbL9oMhm7rQTcusYKjYZjN6081gbHrnxUdu?= =?us-ascii?q?pM2GhmP0iTnxHy5sex+J5s7SFdsO8/+sBDTKv3Yb02QaRXAzo6PW814tbrtQTY?= =?us-ascii?q?QguU+nQcSGQWnQFWDAXD8Rr3Q43+sir+tup6xSmaIcj7Rq06VDi+86tmTgLjhS?= =?us-ascii?q?EaPDA77W7XkNR9gqVVrx2upBJxzY7abp+IOvViZa7dYc8WSHBdUstLTSFNHoWx?= =?us-ascii?q?ZJYPAeobOuZYqpHwp0EPrRqxGwajGfjiyj9SiX/uxa070+AhHh/e3Aw8HtIBrG?= =?us-ascii?q?7YrNLvNKcdV+2+0arGzS3bYv5X1jrx8pXEfx8jrP2WQL58b8TcxVMxGw7KiFib?= =?us-ascii?q?tJbrMCmP1usXtmiW9+pgWvyri24gswxwrD+vxtowioXUn44V0VXE9TlhwIovIN?= =?us-ascii?q?23VlV7YcW+H5tftiGaMYR2Td0kQ2FnuSY6zKMJtYSncygNzZQr3x/fa/qZfIiU?= =?us-ascii?q?+h/uVemcLS1liH9qer+znQu+/Vaux+HmSMW5305Gri9fndnNsnAN2QbT6s+CSv?= =?us-ascii?q?Zl5Eeh2DmO2B7O5exfIUA7j7LbK4Yhw740iJUTqVjDHi7ql0nsi6+WbEok9vCy?= =?us-ascii?q?6+v7erXmuoOcN4hshw7iKKsun8i/Df08MggPRGib5f+x1Kbj/E38WLVFlOc6kq?= =?us-ascii?q?jfsJDAJMQUvLS1AwFP0osl9h2yETOm0MkDnXkbMl1FYg+Jj4noOl7QOP30EaT3?= =?us-ascii?q?v1P5mz5uw7XCP6b9KpTLNHnK1rn7Lphn7EsJ0gsjwNx355tMEqAFLervW0S3s8?= =?us-ascii?q?bXXUxxCBC93+uyUIY17YgZQ2/aWvbIYpOXikeB46cUG8fJYYYUvDjnLP18uKzu?= =?us-ascii?q?hGchiFsQZbWo1t0Qcn/qR606cXXcWmLlh5I6KUlPphA3FbO4iFSaSS9Xam6uXq?= =?us-ascii?q?l64Ss0Wtr/UNXzA7u1ibnE5x+VW51bYmcdUAKTFmr0LsCfXusULiefOdRonT0C?= =?us-ascii?q?WrWnRI4n2Felswqokrc=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BuBgA42hRehxh7k0BmgkSDaAExKo0Mi?= =?us-ascii?q?AaZYYF6CQEDAQwvAQGGKx0GAQQ2BA0CEAEBBAEBAQIBAgMEARMBAQEIDQkIKYU?= =?us-ascii?q?+DII7IoMvGQEBOIEMg2aCeK4eM4J+AQEFgj+DToEeCYE3hz+CFIJFGoIAgREnD?= =?us-ascii?q?AOCL4YChSGvI4JElhIhml+pXIFsAYF2fXGCPlAYDY0sg1mFFIVAQAECMI5dAQE?= X-IPAS-Result: =?us-ascii?q?A0BuBgA42hRehxh7k0BmgkSDaAExKo0MiAaZYYF6CQEDAQw?= =?us-ascii?q?vAQGGKx0GAQQ2BA0CEAEBBAEBAQIBAgMEARMBAQEIDQkIKYU+DII7IoMvGQEBO?= =?us-ascii?q?IEMg2aCeK4eM4J+AQEFgj+DToEeCYE3hz+CFIJFGoIAgREnDAOCL4YChSGvI4J?= =?us-ascii?q?ElhIhml+pXIFsAYF2fXGCPlAYDY0sg1mFFIVAQAECMI5dAQE?= X-IronPort-AV: E=Sophos;i="5.69,407,1571695200"; d="scan'208";a="430297502" X-MGA-submission: =?us-ascii?q?MDGb3cb91VnmUlWpEZsewopJ5uNpcKaNTGDlGR?= =?us-ascii?q?3SZFoC1k5rThaYBiPc43YenNR9YeRUqdQbjjuInahImItyEUZoXLCQ9a?= =?us-ascii?q?ji6WDtQLvrZXjOentLEZ7TiXfVXkLH0OOy9R9ZwC9BDAWJk4ntY8OLDQ?= =?us-ascii?q?URMX+8mtToy2cjvh57XwWopw=3D=3D?= Received: from wout1-smtp.messagingengine.com ([64.147.123.24]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 07 Jan 2020 20:24:59 +0100 Received: from compute3.internal (compute3.nyi.internal [10.202.2.43]) by mailout.west.internal (Postfix) with ESMTP id 594296C5 for ; Tue, 7 Jan 2020 14:24:57 -0500 (EST) Received: from imap2 ([10.202.2.52]) by compute3.internal (MEProxy); Tue, 07 Jan 2020 14:24:57 -0500 DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=happyleptic.org; h=mime-version:message-id:date:from:to:subject:content-type; s= fm2; bh=GphvE9oiH87ffAJslWrJw9tLfuaAw1BFmdvb4Kc44oo=; b=PcC9JSFj 86NeWW8+3HT100l8Xh11s0rp4QAj72pdhWr0QLDVK48OhZfU4YVSvcXHifMHK77B 0KdBNt55uMyh3d61FWDViuqpU+rdvV+0YGriaGgOCamFQzp0kzlZovtBBHU4JTuZ ftjN0oeU3AXeD0sdJcdnQYy3qhcqG0NarOsNAhOyHxOgzv2XfkNiUqKFG7zu83FR pWk+MQCXXVh5iaQVhzr7KE1F7ZAdOoR4Y8seKpV4ZahybjsYa2D0GKgrGq08pYK4 6y6j8iUDp+m6xJiSe3y+crnR0HJqfomrbzjcQpFoOBKqdEa4aFmztMKu7b8wOB7F sMm51sZ0RD0IVQ== DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d= messagingengine.com; h=content-type:date:from:message-id :mime-version:subject:to:x-me-proxy:x-me-proxy:x-me-sender :x-me-sender:x-sasl-enc; s=fm1; bh=GphvE9oiH87ffAJslWrJw9tLfuaAw 1BFmdvb4Kc44oo=; b=afbMDhj04hINnyRMRjwcKaz1HKcZyGc2wTkiw8TsmGDWK 2+VZ04s0zUqfTJra91eUCpxyUU0G4y1USBs4GgAksRR/VwxBo8O/n8EpBmkU+Dmf pN6lTvtbbG1I8+/Lxoq/FxTx/nkUE5I77L0kUH3lLNLsoeg9xsqVr8ElMIV/vRuG xm6Cm+5kWWk8/CxKT/YPN8qogLoV781qWhhHvwOQzW9I6lMkRTybW3qm2CgyqZs4 Xwzwh8aRz8MPlxZvp/G+PpZkq+7h16PgAb/fMAhPsLrQhLZNlZu9PPqArWwjxl1b z6Uby6ItRZ13APTkxtj8L2/2aI16BLwMv1ZIJ3wkA== X-ME-Sender: X-ME-Proxy-Cause: gggruggvucftvghtrhhoucdtuddrgedufedrvdehiedgtdejucetufdoteggodetrfdotf fvucfrrhhofhhilhgvmecuhfgrshhtofgrihhlpdfqfgfvpdfurfetoffkrfgpnffqhgen uceurghilhhouhhtmecufedttdenucenucfjughrpefofgggkfffhffvufgtsehttdertd erredtnecuhfhrohhmpehrihigvggusehhrghpphihlhgvphhtihgtrdhorhhgnecurfgr rhgrmhepmhgrihhlfhhrohhmpehrihigvggusehhrghpphihlhgvphhtihgtrdhorhhgne cuvehluhhsthgvrhfuihiivgeptd X-ME-Proxy: Received: by mailuser.nyi.internal (Postfix, from userid 501) id 8DDE4E00A2; Tue, 7 Jan 2020 14:24:56 -0500 (EST) X-Mailer: MessagingEngine.com Webmail Interface User-Agent: Cyrus-JMAP/3.1.7-731-g1812a7f-fmstable-20200106v2 Mime-Version: 1.0 Message-Id: <4d2b5367-a869-42bc-9547-b58864c10cf8@www.fastmail.com> Date: Tue, 07 Jan 2020 20:24:35 +0100 From: rixed@happyleptic.org To: caml-list@inria.fr Content-Type: text/plain Subject: [Caml-list] Calling a single function on every member of a GADT? Reply-To: rixed@happyleptic.org X-Loop: caml-list@inria.fr X-Sequence: 17932 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'm basically trying to do the equivalent of this simple `fold` function: --- module Simple = struct type term = | Int of int | Add | App of term * term let rec fold i f = function | Int _ as t -> f i t | Add -> f i Add | App (x, y) as t -> f (fold (fold i f x) f y) t end --- ... but using a GADT: --- module Gadt = struct type _ term = | Int : int -> int term | Add : (int -> int -> int) term | App : ('b -> 'a) term * 'b term -> 'a term let rec fold : type a. 'r -> ('r -> _ term -> 'r) -> 'r = fun i f -> function | Int _ as t -> f i t | Add -> f i Add (* ^ Error: This pattern matches values of type (int -> int -> int) term but a pattern was expected which matches values of type int term Type int -> int -> int is not compatible with type int *) | App (x, y) as t -> f (fold (fold i f x) f y) t end --- I've tried other variants of the syntax and got many encouragements but no green flag from the type-checker. Why is the compiler expecting an int term in there? I though the whole point of the `type a. ...` syntax was to allow the matched type to vary from one pattern to the next? Is there a way to do this?