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 5B31F5D5 for ; Fri, 10 Jan 2020 09:50:22 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.69,415,1571695200"; d="scan'208";a="430755019" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 10 Jan 2020 10:50:21 +0100 Received: by sympa.inria.fr (Postfix, from userid 20132) id 573157F3D0; Fri, 10 Jan 2020 10:50:21 +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 78F8E7F345 for ; Fri, 10 Jan 2020 10:50:08 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mmatalka@gmail.com; spf=Pass smtp.mailfrom=mmatalka@gmail.com; spf=None smtp.helo=postmaster@mail-lj1-f173.google.com IronPort-PHdr: =?us-ascii?q?9a23=3AKKoJ0hP4BNRRfob3t6Yl6mtUPXoX/o7sNwtQ0KIM?= =?us-ascii?q?zox0LfX9rarrMEGX3/hxlliBBdydt6sfzbCI6Ou4BiQp2tWoiDg6aptCVhsI24?= =?us-ascii?q?09vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7?= =?us-ascii?q?Ovr6GpLIj8Swyuu+54Dfbx9HiTagb75+Ngu6oATfu8UZnYdvKLs6xwfUrHdPZ+?= =?us-ascii?q?lY335jK0iJnxb76Mew/Zpj/DpVtvk86cNOUrj0crohQ7BAAzsoL2465MvwtRne?= =?us-ascii?q?VgSP/WcTUn8XkhVTHQfI6gzxU4rrvSv7sup93zSaPdHzQLspVzmu87tnRRn1gy?= =?us-ascii?q?ocKTU37H/YhdBxjKJDoRKuuRp/w5LPYIqIMPZyZ77Rcc8GSWZEWMtaSi5PDZ6m?= =?us-ascii?q?b4YXAeoOM+ZWoZfgqVQMoxWwBgajC//0xz9UmnP7x7E23/g7HA3a2gErAtIAsG?= =?us-ascii?q?7TrNXwLKocVvq6zK3UwjXEa/NW3Cr25o/SfRA9u/6MWbFwftDMwkQoEgPFi0+f?= =?us-ascii?q?qZD/MDOR1eQCqXOW7+VlVe21im4nrxt9rSSoxscpk4TEgJ8exFPc9Shh3oo5Od?= =?us-ascii?q?m1RFR4bNOkCpdcqT2WOohsTs8/QWxltj42x78FtJKhfiUHzI4rywDQZvGGaYSE?= =?us-ascii?q?/xPuWPqXLDxlnnxqYqi/iAy38UW4yu3zSM200FFSoypAiNbMt3QN2wXX6siFV/?= =?us-ascii?q?dx50mh1SuN2g3d8O1ELkc0la3UK54l3LE8jIYcsUPGHiPumUX2irGZdlk89+S2?= =?us-ascii?q?9+jqZq/qq5ycOoNulA3yLqcjltaiDek6PAUCR22b9v691L3n8035WrJKjvgun6?= =?us-ascii?q?nctZDVP9gbqbS9Aw9WyIku8Bm/DzK839QZmXkLNk5KeBWCj4TxIVHBPOj4Deuj?= =?us-ascii?q?g1SriDpk2+rJPrjlApnUKnjDkazhfapm5k5HyAszyMhf6IhOBrEAJvLzQE7xu8?= =?us-ascii?q?bCAh83KQzni9rgXfRj34VWdmWTBbGSMKLOqhfc5/wgC+iBaYJTvyzyfasL/fnr?= =?us-ascii?q?2FownVQaeazh+JILYXS7F7wyJkCQfXPogd4pHmIDvw54R+vv3g7RGQVPbmq/Cv?= =?us-ascii?q?pvrgowD5irWMKaHtj00e6xmRyjF5gTXVhoT1WFEHPmbYKBAq5eZyebI8snmTsB?= =?us-ascii?q?B+H4F90RkCq2vQq/8IJJa/LO83RB553m3dlxoebUkENqrGEmP4Gmy2iIClpMsC?= =?us-ascii?q?YISjsxhv4tpEV8zhKH0/E9jaUHTppc4PRGVgp8PpnZnbR3?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0APAQCkRxhehq3QVdFcCR0BAQEJAREFB?= =?us-ascii?q?QGBe4NqXI0MiCeJcXSQUQkBAwEKAQEtAgEBhEACgXAcBwEENBMCEAEBBAEBAQI?= =?us-ascii?q?BAgMEARMBAQEICwsIKYU+DII7KQGCegEBAQIBEhUZARsdAQMBCwYFCwMTJQ8BE?= =?us-ascii?q?xEBBQEcBhMbB4MEgkoBAw4gBJ5ogQM9jCUWBQEXgn8FgkWCCwoZJw1jA4ExAgc?= =?us-ascii?q?JAQiBJIp8gR0agUE/gRGCZS4+hB+GGASNeopnllVHgXqCSJNlG45RjBepSwIKB?= =?us-ascii?q?wYPI4FGgXozGggbFTsxgjtQGA2STxqDWYpUQDOBAiYTkBkBAQ?= X-IPAS-Result: =?us-ascii?q?A0APAQCkRxhehq3QVdFcCR0BAQEJAREFBQGBe4NqXI0MiCe?= =?us-ascii?q?JcXSQUQkBAwEKAQEtAgEBhEACgXAcBwEENBMCEAEBBAEBAQIBAgMEARMBAQEIC?= =?us-ascii?q?wsIKYU+DII7KQGCegEBAQIBEhUZARsdAQMBCwYFCwMTJQ8BExEBBQEcBhMbB4M?= =?us-ascii?q?EgkoBAw4gBJ5ogQM9jCUWBQEXgn8FgkWCCwoZJw1jA4ExAgcJAQiBJIp8gR0ag?= =?us-ascii?q?UE/gRGCZS4+hB+GGASNeopnllVHgXqCSJNlG45RjBepSwIKBwYPI4FGgXozGgg?= =?us-ascii?q?bFTsxgjtQGA2STxqDWYpUQDOBAiYTkBkBAQ?= X-IronPort-AV: E=Sophos;i="5.69,415,1571695200"; d="scan'208";a="335377038" X-MGA-submission: =?us-ascii?q?MDFCN4VoKLxca7+sdrDhHDlAHZ17mG4/s5/PDS?= =?us-ascii?q?IYp+LJz6GB7LcdQhJLfzIMZmN0CT1N6CVVJA+RgyVBuVFYLRtnkFSAFf?= =?us-ascii?q?TV16fsX40DzpdusuA+r70yBgyGqce1IrjvaL17tph8UCatpnOUXFazzA?= =?us-ascii?q?SdzAqnv1ZsUfQ3RmDZov8flg=3D=3D?= Received: from mail-lj1-f173.google.com ([209.85.208.173]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 10 Jan 2020 10:50:06 +0100 Received: by mail-lj1-f173.google.com with SMTP id u1so1474377ljk.7 for ; Fri, 10 Jan 2020 01:50:06 -0800 (PST) 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=EYmowyMu2jz7+OBjHwzeghqlDHkqPh6xrq0KofP2yTI=; b=kMny62R8qJNYGRkzKCUysKzk9pa4nRfnX0cYHQW9tAphC/g53On77V3ncpyo3aeklH EiOkS5MHfT1TFBDzKJOepAhsO7989VbINDJskbNUF36imAgq0xYRiR3kv9SVKKJt1kRX aepU4zn8AjkI5v8JbI+p+yyI5SccUAK2+K0EclvDRwTE0w7HLkciVTJnMJcWYz1VjZfW gMaLtUq2DOAirRJdCB/0slHM+0dEOLr9WfrTqI442r87W9YthC38Jr+78pRWAXO00Ye2 livKv5K7jtW/j0+tBbkzv1dJJEFcEBME6YbPHA6AEJx717AIAGpwCgd+58th4SnK1BVf E6Ig== 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=EYmowyMu2jz7+OBjHwzeghqlDHkqPh6xrq0KofP2yTI=; b=B9q10GnmETWS4pe8em7GILfOWFS1MlagG/ZP58gfHXQRlWDytbDOFk+mHByFjxb7YP 5bRbHn0ziqvPoqcFvvigL258Ox3NClsaWsbDKFwKa6/ydAr4aMa6wcYnSVOvkenqvOVp nAopmAwUZrftN3y6A8WCouQdPOo3Tm18HWEoVOEWT1R6ZID83pxEKksYQ6UTh82orLOK rK7y2K+QWkPLJQ8sTWbt1rr3yrJ9LD8dAOC6eNNumv1hYv3kPSFt5jD4KE2R7ncmTpFi pd+FhSPrWzcvP9TKolipUUSLpUqikQKgtljeM3bETVAw+vSZNtAniXf3Yk/Fb6xMTrKN raig== X-Gm-Message-State: APjAAAXb+D4fw3NGR7MmXqkxU0MOsH+bO/UJ/x4gtAVnWk5fof4ziAg/ dRev6YQlwb/FPEzWCY9tFhA= X-Google-Smtp-Source: APXvYqwU4GthVQnpDymMlTOVbqDPuVG4AX14him/meVR6hPpj+uMRR62sFgo/W7qJFF/z16IeUm7Jg== X-Received: by 2002:a2e:a0d5:: with SMTP id f21mr2074846ljm.106.1578649805729; Fri, 10 Jan 2020 01:50:05 -0800 (PST) Received: from localhost (host-78-79-246-160.mobileonline.telia.com. [78.79.246.160]) by smtp.gmail.com with ESMTPSA id u16sm701205ljo.22.2020.01.10.01.50.04 (version=TLS1_3 cipher=TLS_AES_256_GCM_SHA384 bits=256/256); Fri, 10 Jan 2020 01:50:04 -0800 (PST) References: <4d2b5367-a869-42bc-9547-b58864c10cf8@www.fastmail.com> <41592816-f82e-43a4-b67f-02e69623fe23@www.fastmail.com> User-agent: mu4e 1.2.0; emacs 26.3 From: Malcolm Matalka To: Ivan Gotovchits Cc: rixed@happyleptic.org, caml-list In-reply-to: Date: Fri, 10 Jan 2020 10:49:59 +0100 Message-ID: <86wo9zljy0.fsf@gmail.com> MIME-Version: 1.0 Content-Type: text/plain Subject: Re: [Caml-list] Calling a single function on every member of a GADT? Reply-To: Malcolm Matalka X-Loop: caml-list@inria.fr X-Sequence: 17944 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: Thank you for the explanation Ivan. I have two questions inline. Ivan Gotovchits writes: > It has type `unit -> 'a -> 'a` therefore, if we would have the rank-1 > polymorphism enabled for functions, we could apply it to the function > > let map2 : fun ('a. 'a -> 'a) -> 'b -> 'c -> 'b * 'c = fun f (x,y) -> > f x, f y Small thing, but wouldn't the faux type be the following, based on your usage (making sure I'm following): fun ('a. 'a -> 'a) -> ('b * 'c) -> 'b * 'c > as > > let x,y : string * int = map2 (bad_id ()) "hello", 42 > > and will get a segmentation fault, as `y` will now have type int but hold a > string. > > And here comes the syntax as a savior as it lets us specify functions that > are guaranteed to be syntactic values. Indeed, all three solutions > syntactically guarantee that the provided argument is a function, not a > closure. Indeed, let's introduce the universal identity via a record, > > type id = { f : 'a. 'a -> 'a} > > and we can see that our `bad_id` is not accepted due to the value > restriction, while good_id, defined as, > > let good_id x = x > > is perfectly fine, e.g., > > let id1 = {f = good_id} (*accepted *) > let id2 = {f = bad_id} (* rejected *) > > moreover, even a fine, but not syntactic, identity is also rejected > > let fine_id () x = x > let id3 = {f = fine_id ()} (* rejected *) > > with the message > > This field value has type 'b -> 'b which is less general than 'a. 'a -> 'a > Why is type checking creating a record different than type checking a function argument? If we had the syntax (or something like it): let map2 : ('a. 'a -> 'a) -> ('b * 'c) -> ('b * 'c) Why would the type checker not be able to see that map2 good_id ("hi", 42) is valid but map2 (fine_id ()) ("hi", 32) is not, using the same logic that is verifying creating the "id" record is not valid?