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 5036EE0133 for ; Wed, 31 Aug 2022 10:47:09 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=thiemann@informatik.uni-freiburg.de; spf=None smtp.mailfrom=thiemann@informatik.uni-freiburg.de; spf=None smtp.helo=postmaster@smtp2.informatik.uni-freiburg.de Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of thiemann@informatik.uni-freiburg.de) identity=pra; client-ip=132.230.150.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="thiemann@informatik.uni-freiburg.de"; x-sender="thiemann@informatik.uni-freiburg.de"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of thiemann@informatik.uni-freiburg.de) identity=mailfrom; client-ip=132.230.150.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="thiemann@informatik.uni-freiburg.de"; x-sender="thiemann@informatik.uni-freiburg.de"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@smtp2.informatik.uni-freiburg.de) identity=helo; client-ip=132.230.150.5; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="thiemann@informatik.uni-freiburg.de"; x-sender="postmaster@smtp2.informatik.uni-freiburg.de"; x-conformance=sidf_compatible IronPort-SDR: zikOiARTlPpTGISOgTMiWMu9158DlTJdssgI2+M5ydgst5pKQRUC4bt4FNheUugGv+RuC7ooyH EM7Qz/hQDrF13mxWTW3XTgEw77Z4DUKV+h5vjHxm+TSVhwW2e/TxRL3Fq4HVnQHXgTIhV1Shxd pioJJFLWVGZtT4ZhuRdBeM83D1HB1zTpB0uPXUhEAk0fdCETYKeotBkfdc39O429aEbyEW5TtA doxG3vGD55G5KtxZzVNem1CgsVKsUNNdttKfvTIEyLs7xuGV2pDvNzOkJhy8KEVRsxKF9HDc3s mWeIaiuEGtwZOTg79mqYtER9 X-IPAS-Result: =?us-ascii?q?A0C2AACEHw9jkAWW5oRaFgUBAQEBAQEBAQUBAQESAQEBA?= =?us-ascii?q?wMBAQFAgU+CJIEBVy4EC0WEToh+iBSefwsBAwENMw0CBAEBhQcChGQCHQYGN?= =?us-ascii?q?BMBAgQBAQEBAwIDAQEBAQEBAwEBBQEBAQIBAQIEBAETAQEBAQEBFgkeEA4FL?= =?us-ascii?q?2R0gU+BegYDATANgjUpAYNjAQEBAQIBIx0BATcBBAsLDAwCAhgOAgJXBhOCf?= =?us-ascii?q?QGCfSUDEKgXeoExgQGCCAEBBodpCYERLJASJxyCDYE8DAMNgmc+hESDVjeCL?= =?us-ascii?q?pc3OAMJBAcFLB5CAwsfDhY1HAMUAwUYDAcDGQ8jDQ0EFgcMAwMFJQMCAhsHA?= =?us-ascii?q?gIDAgYVBQICNRg5CAQIBCskDwUCBy8FBC8CHgQFBhEIAhYCBgQEBAQVAhAIA?= =?us-ascii?q?ggmFwcTMxkBBTInEAkhHA4aDQUGEwMgbQUHPg8oMzU5Kx0bCoESKigVAwQEA?= =?us-ascii?q?wIGEwMDIAIQLDEDFAYpExItByt1CQIDImgFAwMEKCwDCT4HKCY8BQVZOgEEA?= =?us-ascii?q?wMQIj0GAwkDAidffpYbg0iBX6FsoGiCHYE/hCSHB5R/IwuFRpEukgIdlmqNO?= =?us-ascii?q?ZVZhE+BeCOBW00kFDsqAYI8CTUQAQIBAQENAQIBAQMBAgECAQgBAQIBjhwZh?= =?us-ascii?q?AyBC4kiPzQ7AgYBCgEBAwmFRoUMAQE?= IronPort-PHdr: A9a23:EcOV2xPsjNu0XmArm5Yl6nZ4BBdPi9zP1u491JMrhvp0f7i5+Ny6Z QqDv64r1g+UFt2Lo9t/yMPu+5j6XmIB5ZvT+FsjS7drEyE/tMMNggY7C9SEA0CoZNTjbig9A dgQHAQ9pyLzPkdaAtvxaEPPqXOu8zESBg//NQ1oLejpB4Lelcu62/689pHJfQlFhzqwbbxuI Bi1sA7cqtQYjYx+J6gr1xDHuGFIe+NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S 6dYDCk9PGAu+MLrrxjDQhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VC+85 Kl3VhDnlCYHNyY48G7JjMxwkLlbqw+lqxBm3oLYfJ2ZOP94c6jAf90VWHBBU95NWCNOH42yb 4kAAeQfMOhXrIf9qUUAoxy5BQS3GOPv0zpIimP23aEm0eksFxzN0gw6H9IJtXTZtM/7O7kOU e+r1qnD0CvNb/NX2Tjj7YjHaBYhofeRVr93bcrRyUgvGB3AjlqKr4zlOSiY1uULs2iV6OpgT +evhHQ7qwFwoTij3Nosio/Iho4MxFDE7zt2wIcuKt2lUk57bsSoH4ZOuCyDMYZ9X8wtTX1yt ikg1r0GpYC0fDIMyJk/xxPSa/yJfYiJ7x/sSeqcIyl0iGx7db+9mxq88Uutx/HhWsS631hHr ChInNnMu34N2RHd5cyKRPRg80qh1ziCywbe4fxKL0AzkKrUMZ8hwrgom5oSt0TDBC72l1/sg K+YbEUp/PWj5ef/Yrj+u5OROZF4hhvgPqkghsCzG/k0PwgSU2SB+emwzKDv8EP2TblQgPA6i LTVvIzEKcgBu6K0DQlY2Zs55RmlFTepytEYkGEHLF1bfBKHiJDkO0rLIPDkFfeznU6gkDZtx /DIOb3hGJDNIWLfkLfgfrZx8VNcyAwyzdxG6ZJUEK8OIPPoVU/srtzYAQU1PBGqzOr/CdV90 J0RWX6XD6OEPq7er0WE6vwhLuWQfoMZpTbwJ+Q/6/PulXM5nEUSfait3ZsZcnC4GfFmLl2FY Xrsg9cOD2IKsRA4TOzsk1CCUDhTZ3i1X6Im4zE0Ep6mDYbARoy3nbyB2ia7EoRYZmBcFF+ME Gznd5ieW/cDci6dP9FuniQCVbe6U4Ahzw2htBfmy7p7KerZ4jMUuYr51Ndp/+3TiQ0y9TtsA sSTy2GNSH10nn8JRzAoxqByuk18ylaG0adjmfxXD8Zf5/JPUgcgNJ7T1fZ2C97oWg7ZZNeGV E6mQsm6ATE2Vt8+38UBY0N5G9m7ihDD3jGqA6MOmryQBJ0097rc0GLrK8Z8zXbGzqghgEM8T stBL231zpJ4oibJDohGlESCoJ6tabgd0TSFoGmZxGyFu0BDFhZ3TbnEUGo3Z03MrN2/6FmUH JG0DrFyCgZdxNTKFqtLZ9jgi1MOEOvjOdnbamS3s2a2CxGSw7qQbYmsZmMcmSvHBUkOjhocu 3qLY1ttThy9qn7TWWQ9XWnkZFnhpKwn8CvTpi4cygiLaxckzL+p4lsPgvfaTfoP37UCsSNnq jNuHV/70ciFQ8GYqV9He6NRKcg4/E8BzXjQ4hB9P5GlJqZkrl8YfQNtukry1hYxF4NB1MYwo XIg0RB9b66Vgxtabz3N+5f2N/XML3XquhWmaqrYwFbbhcqW+6oK4fI+g1TlsgazE0M+8nYhz t9UlnWG65TAERAdF578AQ4s7xYvgbbcb2Em4p/Mk31hNa7hqjjZx9cgH/co0D67estHauWFE gH1CcgTG8mtbvEsmh2ndB8FNv1I++g4MqtKbtOg36imdKZllTOi1yFc5Zxll1iL/Gx6Q/LJ2 JAMx7eZ2BGGXnHylgXptMe/go1CaTwIewj3gSH5GI5cYLFzdocXGC+vJcOw3NB3m5/qXTZR6 leiA1oM3MLhdwCVahTx2ghZ1EJfpnLC+2Pw0zx1njQgqKy33SrAxP7nfQYGOShWQmgng03hI IKpld9cUEXpJwklmR255FrrkrBBrfcaTSGbSkNJci7qamB6B/Lr7PzYOJYJsc5w93gENYb0K UqXQbP8vRYAhibqHm8EgSs+aynvoJLy2RpzlGOaKn936nvfY8B5gxnFt7m+DbZc2CQLQC5gh HzZHF+5apO1/dSZkp7FtMi/UWymTJhabSjoi56GtW61/2BrCwClkLa/l5e0dGpymT++zNRsW SjS+VzgYojm0q28N8pmeEdvHlr198t5XJx4k84+npwR02UAidOZ8DBU9AW7ecUe0qX4Yn0XQ DcNyNOA+wnp1npoKXeRzp74XHGQqid4T/+9ZG5emic07sQQTbyR8KQBhyx+5FyxsQPWZ/F52 DYb0/onrnAA0akPv0I2wyORD6p3fwEQNDHwlxmO89G1rblGLGepf7+q0UNinNenRLicqwBYU Xz9d98sByh1psl4NVvN1jX05OSGMJHMbdMesxSSlT/BieZSMpc4ivsJwzdhOCfzp3AkwfMhg lpi0NDyvYSKLXls4LPsBxdZMjPvYMZAn1Olxa1an8uQw8WuBsA4QW9NBsCwC6v1SHRP5pGFf 06UHTYxq2mWA+/aFA6bsgJ9qm7XVoqsPDeRLWUYytNrQF+cIlZeiUYaRmZf/NZxGwa0ycjma Eo86CoW4wuythtNx+dhMR/XU2HRox2tYys1S96CKhsT4BtP5k3IK8PY4u85TEQ6ttWx6ReAL GCWfVECEWEIV0mNAVbLP7+g4sPF+vSZBayjKfqLb6+DqOZDTfjOyZ/lge4Et36cc86IOHdlF fgy3EFOCGt4F8rukDIKUyULlijJYqZ3vT+a/St65oC6+fXvAkf04JeXTqFVOpNp8gy3hqGKM 6iRgjx4IHBWzMFEw3iA07UZ0FMI7kMmPzCwDbQNszLMR6PMi+dWCRAccSZ6KMpP6eo1wABMP cfRjt692KR/i7Y5DFJMVFqpnc/MB4RCO2amKFbOH1qGLpydICHTmYf2Z627U7hZkORX8QC2u HOVCULiNCmZmH/lWlHnMO1Bij2aIA0LuIy5dUUIayCrR9bnZxundd5v2GRtm/tu3SuMbDNEd 2UvFiEF5qed5i5ZnPhlTmlI734/aPKBhz7c9e7TbJAfrfpsBC1w0eNc+nUzjbVPv0QmDLR4n jXfqtl2rhSoiO6Kn3B7UBtDrz9NgqqKu0tlI6DQ6phDH2vC/VcD92iRAQkQqJ1pB5e83sIYg siKj6/1JDpYppjM+tAAAsHPNM+dGGEkLQKzXj/SAgwfSDe3NGKZmkpc1f+I+3yfs4I17JTh0 slrKPcTRBk+EfUUDV5gFdoJLcJsXz8qprWcidYB+Xu0qBS5rCRypZXbTqjUAPPhLyychKVFZ F0Vx7K9I54eN4fmwUMkZlQoxOwi/mLRW95KuChocg435lhL8T1wVGAy0V//ZUWh7S1LfRZbt h8whAxkZO0x9TSq/lE2Y1TQqSo6jVM+39no02j5TQ== IronPort-Data: A9a23:k+snRKj1fhj3fW2PLDih1CiaX161aBUKZh0ujC45NGQN5FlHY01je htvDTiFOPfeNGegLY0gPN+w8kJQuMWEy9BmSlFo+S4yQStjpJueD7x1DG+gZnLIdpWroGFPt phFNIGYdKjYaleG+39B55C49SEUOZmgH+a6UKieUsxIbVcMpB0J0HqPoMZkxN8z6TSFK1nV4 4mq85aGYAbNNwNcawr41YrT8HuDg9yp4Fv0jnRmDRyclAK2e9E9VfrzFInpR5fKatE88t2SG 44v+IqEElbxpH/BPD8KfoHTKSXmSpaKVeSHZ+E/t6KK2nCurQRquko32WZ1hUp/0120c95NJ Npl9oGPcAgEL7f1qsseEAJzQ3glALxAweqSSZS/mZT7I0zuaH7w268oDUc4Opcd8/p2AidT8 /1dJioAbxqene3wzL/TputE3595apOwZMVG5ykmkFk1Dt5+KXzHa7nK5NJd1TE2rsFIE/HEY sMFaDkpcRLBJhNVN1YdFYgx2uul7pX6W2AA9g/O+vZoi4TV5AUswb73IYDFQc3QWdRlsWCjj GbY8musV3n2M/TElWTZqCv07gPVpgv1QIUOCLy17NZ4gViZ3GVVCRsMVFL9r+PRokW3XtYaL 00P5gI1vK0q/QqqSMP8Vlu2uha5UgU0QN9MC7d86QeDzbDR6hqYBS4ZSD8EZsYrtcUrXzNs2 lLhc87V6SJH86CqcH2w562tnxyxejM+fTZZWD4CdF5QizX8m70bghXKR9dlNae6iNzpBD39q wy3QDgCa6Y70ZFahv3klbzTq238+8eZJuIgzli/Y46z0u9uTKKID2BCwXbB4PdKMZyWBliE9 FIelsmF4+kTZX1mvHPcGbxXdF1Fz9yMPDDaxGFyBYU9+jGn9mSsFb28DRllIVtxaIAFfzHue krapQJSooJVPT6kd6J2aZ+rBIImwMAM9OgJtNiLNbKigbAoKmdrGR2Cg2bMgAgBd2BwwckC1 W+zK5rEMJrjIf0PIMCKb+kcy6Q34Ss12HneQ5v2pzz+j+THNC7JE+xfaAPUBgzc0E9iiFuFm zq4H5XaoyizrMWgMkE7DKZJdQFXdiZjbXwIg5UPJ7TYSuaZJI3RI6SNn+97ItQNc1V9nOrM4 WywElJeyUTyn2bGNRTCbH1/d7T1Xv5CQYETYkQR0aKT8yF7O+6Htf5PH7NqI+VP3LE9nJZcE aJfE+3eWasnd9gy02hBBXULhNc4L0XDaMPnF3bNXQXTiLY8HleVoYa7IFWHGetnJnPfiPbSa oaIjmvzKafvjSw7ZCoPQP7wnV63o1YHn+d+AxnBLtVJIhu+8Y5kLDb0h+M2IIcRLxSGyCGX1 gyLGxheqeSU+90599zAhKalqYa1ErIiTxQAQDSBte67ZXvA426u4Y5cS+LZLznSWVT99Lime egIner3N+cKnQoSvoclS+RrwKsy6sHBvbhfygg4TnzHY07xVOFhJHeBx8xGqqxOgKJfuE64Q E+O8MRANvOFNZq9QlIWIQMkaMWF1O0Vw2WDs65qfR+ivCIupeiJS0RfORWImRdxFrotPdN32 /olte4X9xe720gjPduxhyxJ83iBcy4bWKI9u5BGWILmh1Z5ylxGZpCAWCb67IvUMYdXN1Uye HmVgqTFnbFV2kvBNWc1FD3Dx+dcj4kUt1ZGwQZadViOn9PEgN4x3QFQqGhmEF4Kk08fi+8ja HJ2M0BVJLmV+2k6jsZ0X1ezFlwTHxae4EHwlQcEzTWLU0myW2XRB2QhIuLRrlsB+mdRc2QJ5 r2e02q5Az/mcNuqhHkpXFJ98briS9J27AjLhMGkWdmDHtw0ezfkiLK0aiwEpkK/U882gUTGo 8hs/fpxMPGqa3RP/vdjU4TKh64NTB2kJXBZRa8z9q0+HVbDdWzgwjOJMU2wJJ9AfqSY7U+iB sVyDctTTBDihj2WpzUWCKNkz2WYRxL1CA7uu48HJFLqd5OEqyZx6tTR8Cb5nmoiX9Rt19s7K 8bfbT+DGHGKij1YlgchaSWC1nWQObE5iM/UhYhZM9nl07oCtu9ra0Q7zrq3+WiTMU5p5R+Vt h7ZaOnawoSODGiqc5TESs1+6sbdFT83fOWO/geptt1SbNCJLMHP8g0Pp1jtIh5Ze7ccMziye XJhr/avtH74UH0Kv6w1VnVP+2SlJSl/YQaPDv/KEQ== IronPort-HdrOrdr: A9a23:/BevvKC5pqF9Kp3lHemV55DYdb4zR+YMi2TDGXoBKiC9Ffbo9f xG/c536faQsl0ssR4b+exoVJPvfZqYz/9ICPcqTNKftXjd1FdA/LsSlLcKqgeIc0fDH6xmpM NdmsNFZ+EYY2IK6voSmDPIdeod/A== X-IronPort-Anti-Spam-Filtered: true X-IronPort-AV: E=Sophos;i="5.93,277,1654552800"; d="scan'208";a="50653747" X-MGA-submission: =?us-ascii?q?MDEp/5Mr6HHuCYfWgoDBDSZbohZrZIUsXP2Oz6?= =?us-ascii?q?qWyJsmNwgqfA7VtUShINmAF0neTyb4fsL9gwcG2r0SGizDF6Dnl/AJr6?= =?us-ascii?q?3Ura/nHajxQ+l2ffTxlZxGDMwe53UcyBd0uTQ3Kl0RosoJydJGSezrJi?= =?us-ascii?q?97H4qp9qDC5wNlC3drl2udBw=3D=3D?= Received: from smtp2.informatik.uni-freiburg.de ([132.230.150.5]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/ECDHE-RSA-AES256-GCM-SHA384; 31 Aug 2022 10:47:08 +0200 DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=informatik.uni-freiburg.de; s=mx2204; h=To:References:Message-Id: Content-Transfer-Encoding:Cc:Date:In-Reply-To:From:Subject:Mime-Version: Content-Type:Sender:Reply-To: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=tZ7muqVQRoJeBWXMaFDtDzMHoZTDgAxBCsmPJvs953c=; b=uHo7yGiaFGs0k23K4GqBIt7Xpn TuPCFvyY8NnSJpcPJ5ihb54QIk/86aziaYi6VmvnK3B5xAJGcrbpOz4V0hhhq3IDyq1/GpSBmxrH2 EpK1HaLgsZailtxw7eB792tn+0TwX2aEIoKT2Vuh+JFyHaxMfolyF05wtrRCrATnMAK+JVoDvS2Kr 1oaGs66v4bh8Hv7aCQr9qUzQ79mlDa0zljnZ7536FzhwKjpUjh/ABXH2HwfrzWfmGwdvxfrxvJf4u LGUWw7G6g/j8OJyp/Xy9L1NIMnDBvswja9qNZXvW9loEszU9ZJj8MFflrXwrBXnWVsCcXL36wQgEA sA6yftAg==; Received: from ip-134-003-102-013.um41.pools.vodafone-ip.de ([134.3.102.13] helo=smtpclient.apple) by smtp2.informatik.uni-freiburg.de with esmtpsa (TLS1.2) tls TLS_ECDHE_RSA_WITH_AES_256_GCM_SHA384 (Exim 4.95) (envelope-from ) id 1oTJT7-00077T-2d; Wed, 31 Aug 2022 10:46:59 +0200 Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 16.0 \(3696.120.41.1.1\)) From: Peter Thiemann In-Reply-To: <99c919e0-95aa-2c4f-7240-71486da1fb65@inria.fr> Date: Wed, 31 Aug 2022 10:46:57 +0200 Cc: Peter Thiemann , Andreas Rossberg , caml-list@inria.fr Content-Transfer-Encoding: quoted-printable Message-Id: 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> To: =?utf-8?Q?Fran=C3=A7ois_Pottier?= X-Mailer: Apple Mail (2.3696.120.41.1.1) Organization: Universitaet Freiburg, Institut f. Informatik Subject: Re: [Caml-list] coinductive data types 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.=20= 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 = 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/