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 40AE0E0128 for ; Wed, 31 Aug 2022 20:42:44 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=rossberg@mpi-sws.org; spf=Pass smtp.mailfrom=rossberg@mpi-sws.org; spf=None smtp.helo=postmaster@juno.mpi-klsb.mpg.de Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of rossberg@mpi-sws.org) identity=pra; client-ip=139.19.86.40; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="rossberg@mpi-sws.org"; x-sender="rossberg@mpi-sws.org"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of rossberg@mpi-sws.org designates 139.19.86.40 as permitted sender) identity=mailfrom; client-ip=139.19.86.40; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="rossberg@mpi-sws.org"; x-sender="rossberg@mpi-sws.org"; x-conformance=sidf_compatible; x-record-type="v=spf1"; x-record-text="v=spf1 a:hera.mpi-klsb.mpg.de a:juno.mpi-klsb.mpg.de a:pluto.mpi-klsb.mpg.de a:apollo.mpi-klsb.mpg.de a:jupiter.mpi-klsb.mpg.de a:poseidon.mpi-klsb.mpg.de ?all" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@juno.mpi-klsb.mpg.de) identity=helo; client-ip=139.19.86.40; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="rossberg@mpi-sws.org"; x-sender="postmaster@juno.mpi-klsb.mpg.de"; x-conformance=sidf_compatible IronPort-SDR: MNmIbMIIF+6xA6+0X5dfwA1fXQhOiWvVugG85sviCdIvveTjK/q45WhTznUvcp77yyDefIR+ty lyVXsvinMPEsJObTBiW2kcHpz/jpJSobX9fruKLijFpCxnpJnd9ZyT3q3cwcuRH9O1Oz3IuyRC v9WbHAyU/LlpI9A+6bFfLu1tY61vvqreupHM4X5sql20/FlplvPHpEiUIRaNMLJUzoH93ensAB uhgxh5BWeYb0zy1DmC4HiXEqwcmv+zU734B3UxphUysg6vq18QJ4AxwmBwZCocRlUSE+dn13jT I6PSMag/VMfX4hIZpmjcJZq/ X-IPAS-Result: =?us-ascii?q?A0ARAQCCqg9jmChWE4taFgYBAQEBAQEHAQESAQEEBAEBg?= =?us-ascii?q?g+CJIEBWC0ECxwphE6RDwOefwsBAwENNwgBAgQBAYUHAiKEQgIdBwEENBMBA?= =?us-ascii?q?gQBAQEBAwIDAQEBAQEBAwEBBQEBAQIBAQIEBAETAQEBAQEBAQEUCRkFEA4FP?= =?us-ascii?q?GRkA4FMA4F6BgQwDYI1DBmDYAgBAQEBAgEjHQEBNwEECwsMDBwLAwICRhEZW?= =?us-ascii?q?oIjAYJ9JQMEDKk5eoExgQGCCAEBBoJghQkJgT2IPQGHWCccgg2BPByCMDc+g?= =?us-ascii?q?mIEGIEkAQFNgykUI4IulzAHNwMJBAcFLGMLHw4WZSCBFYFOg2yCAmSBYYEng?= =?us-ascii?q?1SBD4F4gg2BEB8HgicBCoIKfJYkg0gBIAI2DlwcoWygaINchCSHB5UthUaRL?= =?us-ascii?q?gaRfB2kI5VZhE+BTiojgVtNMAg7KgFzCYFACTUQAQIBAg0BAgIDAQIBAgEIA?= =?us-ascii?q?QECAY4cGYRDVINWhUxAMwIBAQE2AgYBCgEBAwmFRgEBAYUJAQ?= IronPort-PHdr: A9a23:ZrvP3xD5euaUEB8gABjGUyQUQEkY04WdBeb1wqQuh78GSKm/5ZOqZ BWZua82ygWZA86Cs6oMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7G MNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+5ZPebx9WiDe+YL5+I wi6oRnNusILnYZsN6E9xwfTrHBVYepW32RoJVySnxb4+Mi9+YNo/jpTtfw86cNOSL32cKskQ 7NWCjQmKH0169bwtRbfVwuP52ATXXsQnxFVHgXK9hD6XpP2sivnqupw3TSRMMPqQbwoXzmp8 qJrSB7ziCccNj459m7XgdFugqxCvRmhqR1/zJDQYI6IKfFyeq3Qcc8fSWdHQ81fVTFOApmkY oUPDOQOIelXoYfgqVQMsxa+Cw6iCfj1xTNUg3/7x6063/gjHAzAwQcuH8gOsHPRrNjtKKoSV /26zLPWwjrZdPNdxCvz6I/TchA6uv6DQ6hwccXMwkQoDQPFiU6QqZf+MDyLzOQNvHOW7+94V eKukmInsA9woiO1yscrkInJiZsYx1bZ/ip23Ig7P8e3SFJnYdG6CptQsTmXOo92TM4sQWxlu zo3x6MGt5O7ciUHypoqyh/QZfGbfYWF/BHuWPueLztlhn9pZrGyiRa9/0agyODwSMm63EtUo ydDj9LCuHcN1xnJ5ciGTPtw5l+h2S2S1wzJ9O5LPF00mbLaK54n2L4wl4AcvV7NHi/snkj9k ayYdl089+S15enqZq/qqoKYOoNuiQzzM74il8OjDeggLAQCQnaX9f6y2bH/50H0TrRHgucrn qTWs53XI9kQqLSjDA9PyIkj7g6yDze439QcmnkKNFBFeA+Bj4juIV3OJej4Dfamj1SvlDdr3 OvJMqfkApXVIXjPiqrucqhl505dzgo808xf6opJBrwPJP//QFL9udjCAhI6MgG42enqBMll2 oMbQ22PA6uZMK3IsV+P4+IiO/OMZIgOuDbmMPcq+eTujXAilF8YZamp3IIbaGu2H/R9OUmZZ mDsgtgZHWcMpQUxVPbqh0GaUT5Pe3ayWLox6iwjBIK8EYjDXpytgKCG3CqjApJZfGVGClSVH XfsdoWEQOsMZTmJIs5hlzwETaKuR5Ug1RGorg/6yqBoIvDa+i0C5trNzt9wssTVmQs//Cc8N cOGyGuAVW48ynkPXCQ80bpwiUllyxKYzrM+hOZXQ48Ar8hVWxs3YMaPh9dxDMr/D1mZFj/oY FOvQ9H8RCo0Usp02dgFJUB0B9SliBnHmSusGb4c0bKRV9Qv6qyJ+X/3Ko5mzmrekrE7hgw8R dBUP2C8iYZ67wmWHJHS1UKDmPXibrwSiRbE73zL1m+SpAddWQ90X7/CWCUFYVDNp9nj6WvHV 77rEqs8dAxbxp3KMbNEP/vui1gOX/L/IJLebma2zn+3HgqNz6iQYZDCeXgb22PYEElBkAQI9 zCDLQd4CirJT3v2KjtoGBqvZkrt9bM7s3anVgouyArMaUR91r2z8xpThPqGSvpV0KhW8CEm4 y55Glqwxbe0Q5KJuhZhcaNAYNg8/EYP1GTXsBZ4N4ChKKYqj0AXcgB+tUfjnxttDYAInc8vp XIshA18TMDQmElGbCiS0Ir/ErjPKyzp4wvpbLTZmxnf3NuQ5qYT+aEgsVyw9AqtF0ck7zBmy 4wMiCrav8SMXFRUDcqiNyR/vwJ3rLzbfCQnsobd1Hk2dLKxrieHwdUiQu0s1hened5bdqKCD g77VcMAVK3MYKQnnUakahUcMaVc7qkxaom8cOCd0qOxM85lhDPjlntcpodn3Qjfkkg0Av6Nx JsDz/yCi0GdUCznhlq7vejygYEBfi4JWG2lxmK3YewZLr03doENB2C0JsSxzdgrnJ/hVUlT8 1u7Dk8H0sukEfaLR2T0xhYYlUEeoHj93DC90yQxiTYi6KyWwC3Jxe3mMhsBIG9CAmd43x/gJ o29jtZSW0bNDUBhjhy+/kz33adzobx+anLMWgFPZSe+I2x5U6S2v6aPeIYWs8Ju6HQRALr6P QjSQ6W1uxYA1iL/A2ZSoVJzPyqnvJn0hV0yiW6QKmpysGuMfMhxwRnF49mPDfVV3zcAWGx5k WyOXQn6ZojvrYvSy8+Q14L2H3isXZBSbyTxmIaJtS/hoHZvHQX6hfe43NvuDQk91yb/kdhsT yTB6hjmMeyJn+y3N/xqek5wCRry8c1/T8tklZArjpwK1lAfnpTQ5mUc12DpPp8IvMC2JGpIX jMNz9PPtUL/31Z4JH+TyKr8TnTY2dR6Id6gbSlFv0B1p9APA6CS4rtemCJzqVfttgPdb892m TIFwOcv4noX0KkZ/RAgxSKHDvUODFFVaGbywg+Q4Yn0/8A1LC6/NKK9301kkZW9AaGe90tCD W3hdM5qFH1w4992dlfU0Tjw7pruPtzIYpQfu3j221/J3epILpV3k+ILwCljImi7uGUqjeI2x RU8xZWnoI/BLn1suaG9GRQeMyX6Ic8en1Olxa8Ml96R24SoWJB5G3AIWIDiC/ewH3QeuLzuZ QSTCDwgp23dHKLeWAyb800gqmrAVZymUhPfbHBL1dJ5SRiRI0oZhRgVGTY+hZR/ExilgsDsO BBw4jRbjrLhgj1LzO8gdxz2U2OF4Rytdi9xUp+Uahxf8gBF4U7Rd82Y9ON6WS9CrNWnq0SWJ 2qXah4tbylBU1GYB13lIril5MXRu+meCO2kKvLSYLKI4eVAXvaMzJir38No5TGJfsmIO3BjC bU81C8hFThhHN/FnjwUVyENvyDQacndoQ+9vy5ztcr59ezkHg7ipMOOB7ZULdRz6kW2jKOEZ IvyzG5yLTdV0I9JxGedkeNOmgdDzXEwMWX1QtFi/WbXQandm7FaFUseYiJ3bo5T6r4kmxNKM ojdg8/00bhxirg0DU1EXBrvgJLMB4RCLmejOVfAHEvOOq6BIGiB2cbseqmxU7J4if1V8gavo nCcCUCpbVHh33H5EguiN+1BlnTRJBtFpIS0aQpgE0DhUdThLBijMZp0iSY8h7gsiTXGOCRPV Fo0O1MIpbqW4yRCh/x5EGEU9XtpI96PnCOB5vXZIJIb2ROEKiFslqdB/298zKFavngsrB1dm jbUqZhru1Djke2UwHxiSBUIpjsZ3OpjWG1nIaSc7YZbH3He80BVhVg= IronPort-Data: A9a23:nXlO5qMJkxZbj07vrR1okcFynXyQoLVcMsEvi/4bfWQNrUon3mQGn zQdWjyPMveONDHzKNF3atjjpxgBv8CBzoJiT3M5pCpnJ55ogZqcVI7Bdi8cHAvLc5adFBo/h yk6QoOdRCzhZiaE/n9BCpC48T8kk/vgqoPUUIYoAAgoLeNfYHpn2EkLd9IR2NYy24DpWFrV4 7senuWGULOb824sWo4rw/nbwP9flKyaVOQw4zTSzdgS1LPvvyF94KA3fcldHFOkKmVgJdNWc s6YpF2PEsw1yD92Yj+tuu6TnkTn2dc+NyDW4pZdc/DKbhSvOkXe345jXMfwZ3u7hB2ost9hy eoWuaa7TEAOPqGQpuVaURhHRnQW0a1uoNcrIFC9rMqUiUjecj7vx+5kSkQuMssU946bA0kXr q1ecWFLPk7F27reLLGTEoGAguw5K9LwNo4FtVll1TCcFuk9B5fZTM0m4PcFhGht2ZgTQp4yY eI/dydGSyzlPycRFVcmLaM/38qUtCHwJmgwRFW9//NsujODnWSdyoPFO9PQfpmORN5Jtl2Jo 3rPuWX/GBATctKFoQdp6Vqum+nI2ybjWccREKaysPtyjxufywT/FSH6S3OajPapi3HlV+hUL gsz+iZyk6l19k20G4yVswKDnFaIuRsVWtx1GuI86R2Qxqe83+p/LjZfJtKmQIJ83PLaVQDGx XfUxom4VGcHXKm9GC7Mr+/8QSaaY3BNRVLucxPoWiMpzrHeTGwbjA/JSZBmCK/wjdnuE3f12 z/MoCVWa1QvYSwjifXTEbPv2m/ESn31ougdu1+/soWNs1kRWWJdT9b0gWU3FN4ZRGpjcnGPv WIfh++V5/0UAJeGmUSlGbtTReH5u6zeaWSN3TaD+qXNERzypRZPmqgPvFlDyLtBaJpUEdMUS BCC6VMOv8E70IWCMPcpO9vZ5zsWIVjIT42+D6uEP7Kik7B9eRKb5ypuaFXY0Wf3i0MsjKcwI pGWbdTEMJrpIfsP8dZCfM9EieVD7nlnnQv7HMmrpzz6j+b2TCPLGN8tbgDUBshnt/zsnekg2 4sFXyd8408BALSWj+i+2dN7EG3m2lBgVMyv950KLbPrz8gPMDhJNsI9CIgJI+RN95m5XM+Rl p1kckMHmlf5m1PdLgCGNiJqZL/1BM8tqGo6eDczJhCvwXd6OdSj66IWdp0We7g79bU6l6QsF qNfJJmNUqZVVzDK2zUBdp2h/oZsQxKm2FCVNC2/bTljIpNtHlSb+tLtcgb12jMJCy676Zk3r 7G6j1qJRIICAh99F4DRcv32lwG9un0UmeRTWUrUI4AKIh+0qdIwdHD816ZlLdsNJBPPwiqh+ zyXWRpI9/PQp4IV8cXSgfzWpYmeFeYjTFFRGHPW7OrrOCTXojijzItHXLradDzRTjmsqqe/Y +ITyun9df4Dh1wMtpJzVbpmlPps69zqrr5c7wJlAHSSMwX1UOw9eCHe0JkdrLBJy59YpRCyB BCF9O5aDqrXasnrJ14mIgd4PP+I0usZm2SM4K1tcln6/iJ+4JGOTV5WY0uXkCVYIbYpYpkpx /wt5Jwf5wCl0EJ4MMuAiWZR72XJLXgbWeMirp5cDIKy0lgnzVRLYJr9DC7q4cjTOosWbRRwe meZ1PjYmrBR5kveaH5tR3LD6upqmspcsh59zGgEKgnbgdHCnPI2gUNcqGxlUgRPwxxb+OtvI Ww3ZVZtLKCD8joAaBKvhIxw99WtxSF1+3AdD3MLiWveCUywVynOKHY3f+OV8wYV/gqwu9SdE K6wkA7YvfTCJakdHRfenWZgs/2mVsNqsArYl6hL2uybSoIib2ONbrCGPAI1RtiOPS/1rEjfp Kxx4/02brf0XcLVT2vXFKHCvYktpNu4yKCujB2vEG7l3Y0RRd1q5QWzFg== IronPort-HdrOrdr: A9a23:uiAeBqvMlY2pArVDZIu4JgIc7skDU9V00zEX/kB9WHVpm5Sj5q eTdPRy73DJYUUqKRcdcLG7SdS9qBznhP1ICOUqUItKGTOW3FdAT7sSkbcKoQeQeREWn9Q1vc wLT0E9MqyUMbEQt6jHCXyDc+rIt+PnzEnHv4vjJjxWPHhXgulbnn9E4hDyKDwMeOBpP+tCKK ah X-IronPort-Anti-Spam-Filtered: true X-IronPort-AV: E=Sophos;i="5.93,278,1654552800"; d="scan'208,217";a="50757057" X-MGA-submission: =?us-ascii?q?MDFK7COVB4rLiUQ48Cd3wJxSv4nnJ7ymDk4eaB?= =?us-ascii?q?pq9cJqFJzwiICZAXDsRxBi5RriC8dFWloJeHLHnijX4AubSHKDgigMIo?= =?us-ascii?q?KmD7dEMpT+YTo3S23oCUh/o7h0ruUjUdOt6f+dzsucKvCUX7p4XAyKx0?= =?us-ascii?q?0yYkk7yvBGv5H1zFR5h7SvoQ=3D=3D?= Received: from juno.mpi-klsb.mpg.de ([139.19.86.40]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/ECDHE-RSA-AES256-GCM-SHA384; 31 Aug 2022 20:42:43 +0200 DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=mpi-sws.org ; s=mail201904; h=References:Cc:In-Reply-To:Subject:Date:Mime-Version: Content-Type:Message-Id:From:sender:reply-to:to:content-transfer-encoding: content-id:content-description:resent-date:resent-from:resent-sender: resent-to:resent-cc:resent-message-id:list-id:list-help:list-unsubscribe: list-subscribe:list-post:list-owner:list-archive; bh=FLr5gx1eCDZx3p4NRtTB4ZY6lu9/bmUbJ1sUJRo+f40=; b=ushOGIg8cUnIkaS59JpRMzHQ4R O65w9nRxxbQfBlXJUJfrN54poVsEoEs8ntSeLEsWUTBS5BJU8pXDMyJ1xM4nr8mNd2srCF7AqV9w2 Xebld1d4j+tgOcITTuVV9ZuaV6JAvoVZ938u41Wdms4nLaNX3KdmgfL2UecIToWbssc8=; Received: from max.mpi-klsb.mpg.de ([139.19.86.27]:49660) by juno.mpi-klsb.mpg.de (envelope-from ) with esmtps (TLS1.3:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.92) id 1oTSfa-00038s-J2; Wed, 31 Aug 2022 20:42:43 +0200 Received: from [212.30.36.148] (port=63272 helo=smtpclient.apple) by max (envelope-from ) with esmtpsa (TLS1.2:ECDHE_SECP256R1__RSA_SHA256__AES_256_GCM:256) (Exim 4.94.2) id 1oTSfZ-00DHQQ-L2; Wed, 31 Aug 2022 20:42:34 +0200 From: Andreas Rossberg Message-Id: <7F00DA21-E7F8-45C6-A3FE-30CDB24A3528@mpi-sws.org> Content-Type: multipart/alternative; boundary="Apple-Mail=_86C6B487-DC36-43AD-A715-DAC8AF0723E4" Mime-Version: 1.0 (Mac OS X Mail 16.0 \(3696.120.41.1.1\)) Date: Wed, 31 Aug 2022 20:42:32 +0200 In-Reply-To: <1e762c7c8645d3b697a82b4a65433fa81e92ee83.camel@clement.pm> Cc: caml-list@inria.fr 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> <1e762c7c8645d3b697a82b4a65433fa81e92ee83.camel@clement.pm> X-Mailer: Apple Mail (2.3696.120.41.1.1) X-RSPAMD-Score: 3.4 (+++) X-RSPAMD-Report: Action: no action Symbol: ARC_NA(0.00) Symbol: RCVD_VIA_SMTP_AUTH(0.00) Symbol: MID_RHS_MATCH_FROM(0.00) Symbol: R_SPF_NEUTRAL(0.00) Symbol: FROM_HAS_DN(0.00) Symbol: MV_CASE(0.50) Symbol: TO_MATCH_ENVRCPT_ALL(0.00) Symbol: MIME_GOOD(-0.10) Symbol: TO_DN_NONE(0.00) Symbol: DMARC_NA(0.00) Symbol: URI_COUNT_ODD(1.00) Symbol: RCPT_COUNT_ONE(0.00) Symbol: MISSING_TO(2.00) Symbol: NEURAL_HAM(-0.00) Symbol: FROM_EQ_ENVFROM(0.00) Symbol: R_DKIM_NA(0.00) Symbol: MIME_TRACE(0.00) Symbol: ASN(0.00) Symbol: RCVD_COUNT_TWO(0.00) Symbol: RCVD_TLS_ALL(0.00) Message-ID: 7F00DA21-E7F8-45C6-A3FE-30CDB24A3528@mpi-sws.org X-RSPAMD-Bar: +++ Subject: Re: [Caml-list] coinductive data types --Apple-Mail=_86C6B487-DC36-43AD-A715-DAC8AF0723E4 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 > On 31. 8. 2022, at 17:55, Basile Clement wrote: >=20 > Hi Andreas, >=20 >> (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.) >=20 > This is interesting to me, do you have a pointer to these discussions = if they are public? Hi Basile, it is public, but scattered around numerous issues, meeting notes, and = presentations in repos of the Wasm github. Not easy to point to a single = place. Happy to try digging something up if you can narrow down what = specifically you are interested in. (I suggest you mail me off-list, = though, since it=E2=80=99s probably off-topic here.) Cheers, /Andreas >=20 > Best, > - Basile >=20 >>=20 >> Best, >> /Andreas >>=20 >> [1] Crary, Harper, Cheng, Petersen, Stone. Transparent and Opaque = Interpretations of Datatypes, 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 >=20 --Apple-Mail=_86C6B487-DC36-43AD-A715-DAC8AF0723E4 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8

On 31. 8. 2022, at 17:55, Basile Clement <basile@clement.pm> = wrote:

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?

Hi Basile,

it is = public, but scattered around numerous issues, meeting notes, and = presentations in repos of the Wasm github. Not easy to point to a single = place. Happy to try digging something up if you can narrow down what = specifically you are interested in. (I suggest you mail me off-list, = though, since it=E2=80=99s probably off-topic here.)

Cheers,
/Andreas



Best,
- Basile


Best,
/Andreas

[1] Crary, Harper, Cheng, Petersen, = Stone. Transparent and Opaque Interpretations = of Datatypes, 1998 (https://citeseerx.ist.psu.edu/viewdoc/summary?doi=3D10.1.1.41.8= 182)


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

Hi Fran=C3=A7ois and Andreas,
this is an interesting question, which we also ran into = quite recently.

Algebraic datatypes seem to = conflate the isomorphism for the recursive type with the injection into = a sum-of-product type for the constructors.
They give = rise to nominal types, not structural.
They are certainly = not equi-recursive, because they are not equal to their unfolding.

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

Best
-Peter


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


Hi Andreas,

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.

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.

In = such a system, an algebraic data type is *not* equal to its unfolding, = which
is why I used the word "iso-recursive".

It is quite possible that I used the wrong = word, and should not have referred
to such types as = "iso-recursive".

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




= --Apple-Mail=_86C6B487-DC36-43AD-A715-DAC8AF0723E4--