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 ESMTP id 910B05D5 for ; Wed, 8 Jan 2020 09:44:23 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.69,409,1571695200"; d="scan'208";a="430390094" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 08 Jan 2020 10:44:20 +0100 Received: by sympa.inria.fr (Postfix, from userid 20132) id 477287F3D0; Wed, 8 Jan 2020 10:44:20 +0100 (CET) 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 E9D2C7F214 for ; Wed, 8 Jan 2020 10:43:34 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jacques.garrigue@gmail.com; spf=Pass smtp.mailfrom=jacques.garrigue@gmail.com; spf=None smtp.helo=postmaster@mail-wr1-f54.google.com IronPort-PHdr: =?us-ascii?q?9a23=3A73l9RhTQNHdR62ZtTGlLWBFnA9psv+yvbD5Q0YIu?= =?us-ascii?q?jvd0So/mwa69bBSN2/xhgRfzUJnB7Loc0qyK6vumAzFQqs7d+Fk5M7V0Hycfjs?= =?us-ascii?q?sXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aFRrwLxd6?= =?us-ascii?q?KfroEYDOkcu3y/qy+5rOaAlUmTaxe7x/IAi4oAnLqMUbgYhvJqktxhbGv3BFZ/?= =?us-ascii?q?lYyWR0KFyJgh3y/N2w/Jlt8yRRv/Iu6ctNWrjkcqo7ULJVEi0oP3g668P3uxbD?= =?us-ascii?q?SxCP5mYHXWUNjhVIGQnF4wrkUZr3ryD3q/By2CiePc3xULA0RTGv5LplRRP0lC?= =?us-ascii?q?sKMSMy/WfKgcJyka1bugqsqRxizYDKboGbN/Rwca3SctwYWWVPUd1cVzBCD46m?= =?us-ascii?q?c4cDE+QMMOReooLgp1UOtxy+BQy0Ce3r0DBHmmb23bAk3OQ6DArI3RYvH8gUsH?= =?us-ascii?q?TVo9X1KbkdWv2ywanK1zrMc+pW2Srj54jTaBwhruuDXahqccrQxkkvCh3Kg06f?= =?us-ascii?q?qYzgJTyV1+ANv3KH4OpnUOKikmgqoBxyrDi33soglJXFi4YPxl3H9Sh12pg5Kc?= =?us-ascii?q?OlREJhYdOpH4NcuzyEO4Z1WM8vR29ltDw7x7AJo5K2fSgHxZI6zBDFcfOHaZKH?= =?us-ascii?q?4hf7WeaRPzh4gHVldaq6hxmo8EigzvTwV8eu0FpXtyZFnNnBu38X2xzc7ciHTf?= =?us-ascii?q?R9/kO/1jqVyw/T7eRELVg1lardNZEh3qY9moQPvUnHBCP7m0X7gLWIekk65+Sk?= =?us-ascii?q?8eTqb7r+qp+ZLYB0iwX+Mqo0msy4BOQ1KgoOUHKH9uSlyb3s41b5TK9FjvIsiK?= =?us-ascii?q?nZqpHaJcsGpqGnGAJV3YMj5Ay+DzeiytgXgX4HLFdddBKdk4fpI03OIOz/Dfqn?= =?us-ascii?q?n1ujijJrx/TfMr3lA5XNNWTDnaz6fbd97k5c0BA8wcpe55JSELEBIej8VlX/tN?= =?us-ascii?q?zCXVcFNFm/yuPjTdF8zZ82WGSVA6bfPrmBn0WP47cNKuKVeYIO8Bn0MeIk6OPj?= =?us-ascii?q?xSs7kFQEYKSym5Qecmq5EelrC0qcaHvoxNwGFDFZ7UIFUOX2hQjaAnZobHGoUv?= =?us-ascii?q?dkv2BpOMedFY7GA7uVrvmE1Sa/EIdRYzkfWF+JGHbsMY6DXqVVMX/AEopaijUB?= =?us-ascii?q?EIOZZcoh2BWp7lKozrNmKq/L4HRdu8+/ktdy4OLXmFc58jkmV53BgVHIdHl9my?= =?us-ascii?q?YzfxFzxLp2+BUvxVKK0Kw+iPtdR4Re?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CKIwAwoxVegDbdVdFmHgELHIF+gT4CA?= =?us-ascii?q?YMDhAmDeoQrhniCEYNuhgN0jleBegkBAwEKAQEvAQGEQAKBaRwHAQQ4Ag0CEAE?= =?us-ascii?q?BBAEBAQIBAgMEARMBAQkNCQgnhUAMgjsigwIBAQEDEhEECwEFCAEbHgMMBgMCC?= =?us-ascii?q?w0CAiYCAiMRAQUBHBMGAgEBHoMAgkYBAy6QA48OgQM9iyZ/FgUBF4J/BYRKChk?= =?us-ascii?q?nDWMDgTECBwkBCHwmAwEBhRqGfA+BTD+BESeCPi4+hElNgkOCXgSNR4sUlkwHg?= =?us-ascii?q?jl1BJUiBhuOTxKMAKk7AgoHBg8jgV2BY00jUDGCO1AYDY0Sg3OKVEAzkHcBAQ?= X-IPAS-Result: =?us-ascii?q?A0CKIwAwoxVegDbdVdFmHgELHIF+gT4CAYMDhAmDeoQrhni?= =?us-ascii?q?CEYNuhgN0jleBegkBAwEKAQEvAQGEQAKBaRwHAQQ4Ag0CEAEBBAEBAQIBAgMEA?= =?us-ascii?q?RMBAQkNCQgnhUAMgjsigwIBAQEDEhEECwEFCAEbHgMMBgMCCw0CAiYCAiMRAQU?= =?us-ascii?q?BHBMGAgEBHoMAgkYBAy6QA48OgQM9iyZ/FgUBF4J/BYRKChknDWMDgTECBwkBC?= =?us-ascii?q?HwmAwEBhRqGfA+BTD+BESeCPi4+hElNgkOCXgSNR4sUlkwHgjl1BJUiBhuOTxK?= =?us-ascii?q?MAKk7AgoHBg8jgV2BY00jUDGCO1AYDY0Sg3OKVEAzkHcBAQ?= X-IronPort-AV: E=Sophos;i="5.69,409,1571695200"; d="scan'208";a="335118355" X-MGA-submission: =?us-ascii?q?MDGAA8ljluz/ik5yOTAVdqOSmzgnN21vD7Yyhx?= =?us-ascii?q?RD0mwdRIvm9VTndd6BnIc064nK6LV1Q+T82qLZ4+C4QgsEiV6AMTjYRy?= =?us-ascii?q?gmtBZcjwE9rNwj/c8GUwrZEs/joeuoYbqbISD0BFfpswUongatc8DT8h?= =?us-ascii?q?nNTB4rqBf2EQIr5Aq1S/IZDw=3D=3D?= Received: from mail-wr1-f54.google.com ([209.85.221.54]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 08 Jan 2020 10:43:34 +0100 Received: by mail-wr1-f54.google.com with SMTP id w15so2631075wru.4 for ; Wed, 08 Jan 2020 01:43:34 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=from:subject:to:references:message-id:date:user-agent:mime-version :in-reply-to:content-transfer-encoding:content-language; bh=BhC6RVk4ZgzbHiRgmqzOL/9cPHr1lRCa9gOocjYyRZ8=; b=NEfd4lD1gG+EbXpyt4hLtSx4IWJbr5etFcpkjdafQfIeJ42ls5sEFQYSGck72Y9l9K 3HZJPAKA0403MvkLzzeGgjnlKFRqgt+KwJMoulE5Q3Qriou954ijVvM6YbVuSRq98K/+ qKKKcnSi8cUOGFwydlTIB99V7MJNENdo1K29Gc3TULw/lU32JpFXyoI505zt0shLm2+D Nbj36E3CEQzqXc0WCF2Ik6dlg/FJ4L5Gspf7G4I37wE3wrwqwQMkh7Y96ZxOyBDeZ5p1 9YmHPLHQZQofPR5sa8Y9QqJBxYIx9cx4v+MH6XLgpIY287/QPDX2OPXZlUeb+vQdRH0X zIUA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:from:subject:to:references:message-id:date :user-agent:mime-version:in-reply-to:content-transfer-encoding :content-language; bh=BhC6RVk4ZgzbHiRgmqzOL/9cPHr1lRCa9gOocjYyRZ8=; b=OZ4NWJoml5X1HHNG92mAHjw8ww4MfKCYzcXSASslFgI1EiI8sS7JFKhC+/ad2okoMO rudVLz3eU0G0UBLdgGbg2xesG7z/IYbyNGyar67bycVq9hyhcT7pHwmUW++3HAUZ/gmf Gh71sioBlN6x/coNH+taI3xebz7XTrVUDyucNXiVgtTbXWZg7JovGQhtF3og0aRUfopi m0ueyfcACwj/RlsuMsLAZqs6//t0Zel0Q0yQwW40ZbP1OBLx16unbKmyrOpeN11oV/vf JcSqQ7NtVu5d0gJ5HSSOSJjZNVq1JU9Vuj8c+KqR4GIaSfaLe8URl2X3h+3SJCOe4ca/ 0mcg== X-Gm-Message-State: APjAAAU6miB0Y8oOWbLQUftW8zTiKmF2BirVnwCVOrSYSkDTu3YIaJfq K24RwUXW/0jODZyOCKETMigG4gxHGe4= X-Google-Smtp-Source: APXvYqw4M1wTJ5q/tX2p5TGr6tvKqc3eG9+saSYgQZIlbfjvH87KfIL4ZdQjNt5+SOQj79PKMyMF4g== X-Received: by 2002:a5d:5706:: with SMTP id a6mr3358049wrv.108.1578476613275; Wed, 08 Jan 2020 01:43:33 -0800 (PST) Received: from [128.93.64.65] (sauternes.paris.inria.fr. [128.93.64.65]) by smtp.gmail.com with ESMTPSA id f1sm2226537wmc.45.2020.01.08.01.43.31 for (version=TLS1_3 cipher=TLS_AES_128_GCM_SHA256 bits=128/128); Wed, 08 Jan 2020 01:43:31 -0800 (PST) From: Jacques Garrigue X-Google-Original-From: Jacques Garrigue To: caml-list@inria.fr References: <4d2b5367-a869-42bc-9547-b58864c10cf8@www.fastmail.com> <41592816-f82e-43a4-b67f-02e69623fe23@www.fastmail.com> Message-ID: <0096d024-b800-375b-938e-0ce53cddad87@gmail.com> Date: Wed, 8 Jan 2020 10:43:31 +0100 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:68.0) Gecko/20100101 Thunderbird/68.2.2 MIME-Version: 1.0 In-Reply-To: <41592816-f82e-43a4-b67f-02e69623fe23@www.fastmail.com> Content-Type: text/plain; charset=utf-8; format=flowed Content-Transfer-Encoding: 8bit Content-Language: en-US X-Validation-by: jacques.garrigue@gmail.com Subject: Re: [Caml-list] Calling a single function on every member of a GADT? Reply-To: Jacques Garrigue X-Loop: caml-list@inria.fr X-Sequence: 17935 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: Actually, this is a rare case where using a polymorphic method may be handy too: let rec fold : type a r. r -> 'b term -> r> -> a term -> r =     fun i f -> function     | Int _ as t -> f#v i t     | Add -> f#v i Add     | App (x, y) as t -> f#v (fold (fold i f x) f y) t let v =   object method v : type a. _ -> a Gadt.term -> _ =     fun x -> function       | Int n -> x+n       | Add -> x+1       | App _ -> x+2   end let r = Gadt.fold 0 v (App (App (Add, Int 3), Int 5)) The point being that to match on a Gadt you will anyway need to use the (type a) construct to allow refinement. Jacques On 08/01/2020 07:54, rixed@happyleptic.org wrote: > Hello and thank you for the answer. > > On Tue, Jan 7, 2020, at 21:21, Ivan Gotovchits wrote: >> It is the limitation of the let-bound polymorphism. (...) >> In your case, I would define a visitor type, e.g., >> type 'r visitor = {visit : 'a. 'a term -> 'r -> 'r} > Oh I see. I've used this trick to force a function to be polymorphic, but I failed to see that this was the problem because to me `f` is not any more polymorphic when the `term` is a GADT than when it's not. > > So there is no lighter syntax to specify that `f` should accept any member of a GADT than the syntax to specify that `f` should accept any type at all? > > I wonder, is this just a limitation of the OCaml parser or is there some deep reason for these work-around (like is the case, from my understanding, for the value restriction)? > > Sorry for asking such simple questions but I've build a mental model of how OCaml type checking works mostly from trials and errors, which used to work great until some versions ago :)