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 sympa.inria.fr (Postfix) with ESMTPS id E3897E0128 for ; Wed, 31 Aug 2022 17:55:38 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=basile@clement.pm; spf=Pass smtp.mailfrom=basile@clement.pm; spf=None smtp.helo=postmaster@tobiko.clement.pm Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of basile@clement.pm) identity=pra; client-ip=5.9.79.153; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="basile@clement.pm"; x-sender="basile@clement.pm"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of basile@clement.pm designates 5.9.79.153 as permitted sender) identity=mailfrom; client-ip=5.9.79.153; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="basile@clement.pm"; x-sender="basile@clement.pm"; x-conformance=sidf_compatible; x-record-type="v=spf1"; x-record-text="v=spf1 ip4:5.9.79.153 ip6:2a01:4f8:161:9281:1000::/68 -all" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@tobiko.clement.pm) identity=helo; client-ip=5.9.79.153; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="basile@clement.pm"; x-sender="postmaster@tobiko.clement.pm"; x-conformance=sidf_compatible IronPort-SDR: 3ffgyCGIX+iICs1dreOIy1JFw9wxw1GK0aRis0weTSXJ94CIaMkaIARjkkcOIyQc9sDOQtcs2J N9bv1aTvSmmcrn9N7c5CWgN5zDb2WYKfHhmMXhYmB66/mMBYU+N6QKJQnAhj+WLn5TXWE3SOg8 agPxRqD7FKwE1khhDQuDSdNzXapZXV6RSHLF0CPcVTf0fV07b059oemAENXLRFberxVLxSrwoC gD+vGzuO+9qwRx0O6JrK9lKecoNOcRaGhiepfVRnidAnR6jainvtrauRBIJUbblrfgNfwnatHc zqn4kJOE2W0dGZe9YBfzCzhU X-IPAS-Result: =?us-ascii?q?A0A9BAB9gw9j/5lPCQVaFggBAQsSDIQzB3pXLgQLRYROk?= =?us-ascii?q?RIRnm4LAQMBDTcIAQIEAQGFBwIIhFwCHQcBBDQTAQIEAQEBAQMCAwEBAQEBA?= =?us-ascii?q?QMBAQUBAQECAQECBAQBgQgtZGQEgUsEgXQLNA2CNSkBg2MBAQEBAgEjZgsYK?= =?us-ascii?q?gICVwYBEoJ+gn0lBwELqRZ6gTGBAYRxgyyBZYE9iD0BAYMzhCQnHD+BToQIN?= =?us-ascii?q?z6CYgQYhRyCZQSXLAc3AxorHkIDC3cDFwMUAwUYDAcDGQ8jDQ0EFgcMAwMFJ?= =?us-ascii?q?QMCAhsHAgIDAgYVBQICTTgIBAgEKyQPBQIHLwUELwIeBAUGEQgCFgIGBAQEB?= =?us-ascii?q?BUCEAgCCCYXBxMYGxkBBVkQCSEcDhoNBQYTAyBtBQo7DygyNTkrHRsKgRIqK?= =?us-ascii?q?BUDBAQDAgYTAwMiAhAsMRQGKRMSLQcrdQkCAyJoBQMDBCgsAwkhHwcoJjwFB?= =?us-ascii?q?Vk6AQQDAxAiPQYDCQMCJ119liODSAEggT6XD4pdoGiDXIFFiWaVLYFEhAKRL?= =?us-ascii?q?AiRfB2WaiCNGZoogT85JYFZMxoIMDuCZwlFAQIBAg0BAgIDAQIBAgkBAQKSe?= =?us-ascii?q?VSJIj80AgEBATYCBgEKAQEDCYVHAQGFCQEB?= IronPort-PHdr: A9a23:SOnXAhODlkZCYs3nOLcl6nagBhdPi9zP1u491JMrhvp0f7i5+Ny6Z QqDv64r1g+XFtuFo9t/yMPu+5j6XmIB5ZvT+FsjS7drEyE/tMMNggY7C9SEA0CoZNTjbig9A dgQHAQ9pyLzPkdaAtvxaEPPqXOu8zESBg//NQ1oLejpB4Lelcu62/689pHJfQlFhzuwbbxzI Ri3sA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S 6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VC+85 Kl3VhDnlCYHNyY48G7JjMxwkLlbqw+lqxBm3oLYfJ2ZOP94c6jAf90VWHBBU95SWSJcAo2yc YUBAOgPPelEoYbyqEADogGiCQS2Hu7j1iVFi33w0KYn0+ohCwbG3Ak4Et8TqnvUt9T1NKMMX uuo0qTIySvMb/ZI1jf79IjDbxcsruqWUrJrcMrRzVcgGhjZgVWUt4PlOi2a1uIRs2SB9+pgU Puihmg6oA5+vjah3N0jipXVho0L0FDE8z10zYgpKdC7S0N2b96qHYdfuiyGOYV6XMIvTWFnt ionxLMLpIK3ciYJxZk6yRDSauKLfomW7x/tSeqdPSl1iW9hdb+5mh28/0+gyujmWcm11lZHt jJFksLRtnwXyRPc99WHRuN8/kenwzaP1hrc5vtKIUAuk6fQNp0vwqYom5cTq0jOGjX6lUfyg aOMa0kp+ual5/zjb7n4vJOQKo55hwXkPqgzlcGyAf40PhYOUmSG/+m3yaft8lfjQLpQi/07i qnZv47eJcQcvqO5HwhV3Z0i6xa8CDeqysgXnX0ZI1JAZh2HiZTpN0vWIPD9Ffu/glKsnyl3x /3ePrDtGJHAImLBnbrlZ7px9k5RxQQrwdBa/Z1UC7UBIPzpWk/2sdzVFgQ2PBavw+bmDNVyy JgTVn6LAqCHNaPdr1mI5v41L+mUYY8ZoDD9JOM96P70kXA5gUMdfbWu3ZYPdXy0Bu5mLFmBY XrwntcBFn8HsRYkQ+zvjF2OSDpTZ3epX6Ig/Tw7E4KnDYLbRo+3mrCB3SG7HodXZm9cEFyMH 23oJM24XKIHYSeWZ8tgiSAsVL67SoZn2wvq/Cb8x6BqJ/GcwCoDrpjuztc9s/fUjgo4+CZ7J 8GF0iSWUHoymXkHEWwYxqd69GZ00VaH3OBTh/FdGNpPr6dDWxw7MZP0xOh3Dt30RkTZe4HaG x6dXty6DGRpHZoKyNgUbhM4Qo365vii9y+jArtP0qeOGIRx6KXXmX74O8d6zX/CkqgnlVgvB MVVZiW9nqAq0Q/VCsbSllmB0b6wfPEW1TXM8Gqrxm6DuUxeTEhoVPaNRmgRM3Pfts+x/UbeV /mrALUjPBFGzJuII7BLbtDBhlFLQfrlJJLGZjH5gH++UDCPwL7Ed4/2YyMd0SHaXVADiBwW9 G2aOBIWGiCromHZSjdqGFfiZV+q6ewWRGqTaEgywknKakRg0+Dw4RsJnbmGTPhV2LsYuSAno jEyHVCn3tuQBcDS7wxmNL5RZ98w+jIlnSrQqhB9M5q8Lqtjmk9WcgJ5uFnr3gl2DYMImNYjr Xcjxg5/YayC11YJezSd1JH2crrZTwu6tBqmcK/S13nV1NuT96ETruw96h3isAyvCks+4iB/y dAGm3CY55jMEE8TScesFBdxqEk8/uyBMUxfr8vO2HZhMLe5qGrH0tMtXq4+zwq4Os1YO+WCH RPzFMsTA46vLvYrkh6ndEFhXqga+agqMsehb/bD1rSsObMqlju9jGBKyIt530eB8TY6UuuCj PNni7mImxCKUTvxlgLruMnsmIRJTToWE2+yzzSiHIsbNeViOI0MD2mpOci+wN5z0oXsV3Bv/ 1mmH1oa2cWtdHJ+dnTF1BZLnQQSqH2jw26jyiBs1isupeyZ1TDPxOLrcFwGPHRKTS9slwWkL Y+xhtEcFE+mCmph3BGs/kf+yoBQoKl6Im/PB19NNyT7NGBtVKKsu6HKPogersx593wKC6y1e hiCR6T4ogcG3i+rBGZYyD0hNlTI8t34kxF8lGOBPSN2pXvdd9t3wESX79jdSPhNmzseEXQ+2 H+IVx7lYoL6mLfc343Oue2/SW+7A5hacC2xiJiFqDP+/2phRxu2g/G0nNTjVwk8yy7ykddwB kCq5F7xZJfm06OiPKdpZE5tURX24tF7HoxWmY89gZwWxT4Cg9/GmBhP2Xe2Kthd1a/kOTAHT CUKx9P96wzo3UBlMjSRwsiqHmXYycxnad6gZ2oQ0S9o9MFGBpCf67lclDd0qF61/mezKbBt2 y0Qwvw05DsGkvkE7UAzmz6FDOlYTgFIeDbhnBOS45WiobVLMSyxJKOo2hM2nMj9XuzE80cDC TCgJ8xHf2c4790hYgjFiCShto+0KoCONIBC7E3NwU6Y17AHetVvxrJPjC5jcwoRpFUDzOg2x Vxr1JC+5s2cLnl1ubi+CVhePyH0YMUa/nfsi7xfl4CYxdLnGJIpATgNUJbyKJDgWDsPqfTqM RqPGzwguz+aH7TYBwqW9EZhqTrGDZmqM3idIHRRw89lQVGRI0lWgQZcWztf/NZxDgex2Mnoa 1t0/BgN4VT5qRwKweZlMhT5TiHHoUbgazs5ToSeMAsD7gxG4BSwU4TW5eZyEidEu5y5+VHLe yrENkIRUDpaPy7MT0ruNbSv+9Tapu2RB+7kauDLfa3Ls+tVEfGB2ZOo1IJiuTeKLMSGeHd4X JhZkgJOW250H8PBlnABUSsSwmjHZtWaoBqU8Sl6q8257LLzXUi8gOnHQ6sXKthp9x2s1O2bM PWMgS9iNTtC/o8Lz37Lz/4U2FMXhidyMSGoW+dl12aFXOfbnalZCAQeYiV4OZ5T7q4y6QJKP NbSltL/0rMQZh8dF1BPVF/m3MqtaMkHJX37LFaVXC5j25yNITDOzsfrJ7u5G+Q4ZAB8vBm9v DudDwn7O2bb/wQ= IronPort-Data: A9a23:gWApdK5ztUQTN4JZDcacVAxRtKTAchMFZxGqfqrLsTDasY5as4F+v jBJDWGHMvrZYzejLo10YNu0pkMCu5fVyN9nSlBvqSFgZn8b8sCt6faxfh6hZXvKRiHgZBs6t JtGMoGowOQcFCK0SsKFa+C5xZVE/fjUAOK6UoYoAwgpLeNeYH5JZSlLxqho2eaEvfDjW1nX4 YOp+pWFULOY82cc3lw8u/rrRCxH56yaVAMw5jTSstgW1LN2vyB94KM3fcldHVOgKmVnNrLSq 9L48V2M1jixEyHBpT+Suu2TnkUiGtY+NOUV45Zcc/DKbhNq/kTe3kunXRYRQR8/ttmHozx+4 OcWk5+1dDcGApT3uupDUh9zTAclJrITrdcrIVDn2SCS51HBeXrvxLNlCEwzMIsEvP5yaY1M3 aFeeXZSP1ba2rneLLGTEoGAguwpJdLqOI43sXVtyDzfEbA+RPgvRo2XvYADjWxg2KiiG96ES e03ciYwfi/YYkxRBHQdA4Ak38a30yyXnzpw8wvI+vFsuAA/1jdZ27HoNJ/Re8eWbd5Em16R4 GPA5WXwRB8AXOFz0hKZ9XitheiJlif2XY8UCPug85aGnWF/2EQhUzsVUGaLjsWAsWywBdNZA BMyoTEx+P1aGFOQcjXtY/GpiCfa4EdMB4AKTLxSBBKll/OOslfCboQQZm8dOYV+3CMjbWZyj je0c8XV6StHnJD9dJ58ylt3hWrjUcTtBTVeDRLotCNcizUZnKk9jwjUUvFoG7Ovg9v+FFnYm m7U9Xhu2+9I1JdSic1XGGwrZRr8/PAlqSZlvG3qsp6Ns1IRiHONPdfyswSEsZ6s0q7JEQLe4 xDoZPRyHMhVVMzSz3fWKAn8NLGk++SDPSeUhlhrHp8svzuo8X7LQGyjyGEWGaudCe5aI2OBX aMlkV4JvMc70brDRfQfXr9d/OxxnPS5SYW4Da28gxgnSsEZSTJrNRpGPSa4t10BWmB1+U3mE ZvEI8uqE1gADqFrkGi/S+sHiOd5zSQzwG7VWdbjyk3/g7aZYXeUT5YDMUePN7tlt/Pe/V6Kq tsPZdGXzxh/UfHlZnWF+4AkK11Xf2MwAor7qpAKe+PaelhmFWgtBuX/27Qkf4A5za1Zmv2Rp iO2XkJdxVzjw2XCcF3YZndmYbLpfJB+sXNiZnB3bQz1gCd6bN/2vqkFdpYxcb02z8BZzKZ5H 6sfZsGNIvVTUTCbqT4TWp/w8d55fxOxiAPSYieobWRtf5NkQACVqNbochG2q3sSCSC2tsx4q Lmt0w7dXdwbQl06XsrRbfuuyXK3vGQcwbkuBBuSf4IMIUi8opJ3LyHRj+MsJ59eIxv0xgyci 1ScDyAeqLSfuIQy6tTI2fuJotv7Ced4BUYGTWDX4azvanvG+WCiwogGW+KFeD3bSCXs/fz6N +lSyvj9NtwBnUpL6tEgSOYxkPlhvta/9aVHyglEHWnQawr5AL1XIk6AgZtFuJpLy+ILogCxQ E+OpoJXNLjh1BkJy7LNyNfJr9hv1M34XhHO6v40I0K87yt6+beBTQNKOnFgTcCbwKRdaOsYL SUJ4ab6KDBTTjIhNtuDgyZIsXyJRpDFe7tyrYkUWecHlSJyomyvovXg5uve65WCbthKLg8yJ 1d4QUYEa6t0niL/Tpb4KZQBMSexS3jDVNCmAWLu/2i0p+c= IronPort-HdrOrdr: A9a23:P04rM6lRcSiIzinWKOnjqelZ65rpDfIn3DAbv31ZSRFFG/Fw9v re+MjzuiWE6wr5NEtApTnEAtjjfZq+z+8S3WByB9iftWDd0QPCQe1fBMnZsljd8kbFmNK1u5 0BT0EzMqyWMbGkt6zH3DU= X-IronPort-Anti-Spam-Filtered: true X-IronPort-AV: E=Sophos;i="5.93,278,1654552800"; d="scan'208,217";a="50739386" X-MGA-submission: =?us-ascii?q?MDHfIGFtTWezE2hBG+dGsNUfuCxTFtrd9FJX4u?= =?us-ascii?q?/H1qqtNNs/uxmGaLmjGWUqJdCoUzJI/tYdlJ1RwQZXhpZugoSOhjuf8g?= =?us-ascii?q?WO++zFmty9yOoPxOa76FTjLa2+AzGKgkxbEfjC1klGG1bFuJ1pzlmRmf?= =?us-ascii?q?fWV1V9WStk0ifVEuFyrO5W7w=3D=3D?= Received: from tobiko.clement.pm ([5.9.79.153]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/ECDHE-RSA-AES256-GCM-SHA384; 31 Aug 2022 17:55:38 +0200 Received: from localhost (localhost [127.0.0.1]) by tobiko.clement.pm (Postfix) with ESMTP id DE65B202A7; Wed, 31 Aug 2022 17:55:37 +0200 (CEST) X-Virus-Scanned: Debian amavisd-new at clement.pm Received: from tobiko.clement.pm ([127.0.0.1]) by localhost (tobiko.clement.pm [127.0.0.1]) (amavisd-new, port 10024) with LMTP id HcV9d6FJhObs; Wed, 31 Aug 2022 17:55:36 +0200 (CEST) Received: from [192.168.1.18] (lfbn-idf2-1-1333-251.w92-169.abo.wanadoo.fr [92.169.145.251]) by tobiko.clement.pm (Postfix) with ESMTPSA id E724D201ED; Wed, 31 Aug 2022 17:55:35 +0200 (CEST) Message-ID: <1e762c7c8645d3b697a82b4a65433fa81e92ee83.camel@clement.pm> From: Basile Clement To: caml-list@inria.fr, Andreas Rossberg Date: Wed, 31 Aug 2022 17:55:35 +0200 In-Reply-To: <9C63A771-E4AD-42E4-A889-56CB1FFB563E@mpi-sws.org> References: <25e68e2c-04d2-7764-e189-00812c08a34a@inria.fr> <8078ad33-f220-b233-4863-06ce30cc8cff@inria.fr> <2C890C66-F8F7-402C-B88E-587C3E21DE89@mpi-sws.org> <99c919e0-95aa-2c4f-7240-71486da1fb65@inria.fr> <9C63A771-E4AD-42E4-A889-56CB1FFB563E@mpi-sws.org> Content-Type: multipart/alternative; boundary="=-q/PczNbiPIdJbZrZzi6F" User-Agent: Evolution 3.44.4 MIME-Version: 1.0 Subject: Re: [Caml-list] coinductive data types --=-q/PczNbiPIdJbZrZzi6F Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable Hi Andreas, > (I=E2=80=99ve been rather interested in this topic lately, because the > semantics of type recursion has been a highly contentious issue for > WebAssembly, until we settled on an iso-recursive semantics. The > difference between iso-recursive and nominal becomes rather crucial > once you need to compile structural source types into them =E2=80=93 then= a > nominal semantics in the target language essentially breaks separate > compilation/linking.) This is interesting to me, do you have a pointer to these discussions if they are public? Best, - Basile >=20 > Best, > /Andreas >=20 > [1] Crary, Harper, Cheng, Petersen, Stone.=C2=A0Transparent and Opaque > Interpretations of=C2=A0Datatypes, 1998 > (https://citeseerx.ist.psu.edu/viewdoc/summary?doi=3D10.1.1.41.8182) >=20 >=20 > > On 31. 8. 2022, at 10:46, Peter Thiemann > > wrote: > >=20 > > Hi Fran=C3=A7ois and Andreas, > >=20 > > this is an interesting question, which we also ran into quite > > recently. > >=20 > > Algebraic datatypes seem to conflate the isomorphism for the > > recursive type with the injection into a sum-of-product type for > > the constructors.=20 > > They give rise to nominal types, not structural. > > They are certainly not equi-recursive, because they are not equal > > to their unfolding. > >=20 > > I'd also call them iso-recursive or should they be a category by > > themselves? > >=20 > > Best > > -Peter > >=20 > >=20 > > > On 31. Aug 2022, at 10:25, Fran=C3=A7ois Pottier > > > wrote: > > >=20 > > >=20 > > > Hi Andreas, > > >=20 > > > Le 30/08/2022 =C3=A0 18:45, Andreas Rossberg a =C3=A9crit : > > > > I=E2=80=99m curious why you would categorise iso-recursive types as > > > > nominal. I have always considered them structural as well, > > > > since two structurally matching iso-recursive type expressions > > > > are still deemed equivalent. > > >=20 > > > I had in mind a system with algebraic data types, which have a > > > name, and where > > > two algebraic data types with distinct names can never be related > > > by subtyping. > > >=20 > > > In such a system, an algebraic data type is *not* equal to its > > > unfolding, which > > > is why I used the word "iso-recursive". > > >=20 > > > It is quite possible that I used the wrong word, and should not > > > have referred > > > to such types as "iso-recursive". > > >=20 > > > -- > > > Fran=C3=A7ois Pottier > > > francois.pottier@inria.fr > > > http://cambium.inria.fr/~fpottier/ > >=20 >=20 --=-q/PczNbiPIdJbZrZzi6F Content-Type: text/html; charset="utf-8" Content-Transfer-Encoding: quoted-printable
Hi Andreas,

(I=E2=80=99ve = been rather interested in this topic lately, because the semantics of type = recursion has been a highly contentious issue for WebAssembly, until we set= tled on an iso-recursive semantics. The difference between iso-recursive an= d nominal becomes rather crucial once you need to compile structural source= types into them =E2=80=93 then a nominal semantics in the target language = essentially breaks separate compilation/linking.)
<= div>
This is interesting to me, do you have a pointer to thes= e discussions if they are public?

Best,
= - Basile


Best,
/Andreas

[1] Crary, Harper, Cheng, Petersen, Stone. Transp= arent and Opaque Interpretations of Datatypes, 1998 (ht= tps://citeseerx.ist.psu.edu/viewdoc/summary?doi=3D10.1.1.41.8182)


On 31. 8. 2022, at 10:46, Peter Thiemann <thiemann@informa= tik.uni-freiburg.de> wrote:

Hi Fran=C3=A7ois and Andrea= s,

this is an interesting question, which we a= lso ran into quite recently.

Algebraic datatyp= es seem to conflate the isomorphism for the recursive type with the injecti= on into a sum-of-product type for the constructors.
They giv= e rise to nominal types, not structural.
They are certainly n= ot equi-recursive, because they are not equal to their unfolding.

I'd also call them iso-recursive or should they be a c= ategory by themselves?

Best
-Pet= er


<= div>On 31. Aug 2022, at 10:25, Fran=C3=A7ois Pottier <francois.pottier@inria.fr> wro= te:


Hi Andreas,
<= br class=3D"">Le 30/08/2022 =C3=A0 18:45, Andreas Rossberg a =C3=A9crit :
I=E2=80=99m curious why = you would categorise iso-recursive types as nominal. I have always consider= ed them structural as well, since two structurally matching iso-recursive t= ype expressions are still deemed equivalent.

I had in mind a system with algebraic data types, wh= ich have a name, and where
two algebraic data types with dist= inct names can never be related by subtyping.

= In such a system, an algebraic data type is *not* equal to its unfolding, w= hich
is why I used the word "iso-recursive".
It is quite possible that I used the wrong word, and should no= t have referred
to such types as "iso-recursive".

--
Fran=C3=A7ois Pottier
francois.pottier@inria.= fr
http://cambium.inria.fr/~fpottier/


=

--=-q/PczNbiPIdJbZrZzi6F--