From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 B56A3E0128 for ; Wed, 31 Aug 2022 17:40:53 +0200 (CEST) Authentication-Results: mail3-smtp-sop.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 (mail3-smtp-sop.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=mail3-smtp-sop.national.inria.fr; envelope-from="thiemann@informatik.uni-freiburg.de"; x-sender="thiemann@informatik.uni-freiburg.de"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.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=mail3-smtp-sop.national.inria.fr; envelope-from="thiemann@informatik.uni-freiburg.de"; x-sender="thiemann@informatik.uni-freiburg.de"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.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=mail3-smtp-sop.national.inria.fr; envelope-from="thiemann@informatik.uni-freiburg.de"; x-sender="postmaster@smtp2.informatik.uni-freiburg.de"; x-conformance=sidf_compatible IronPort-SDR: 0Tqxeu1smBVO81Bi3UMOPxO6Ynq8atfjMVuPigYdICgMZ5a7qIAv5+PKVfeAcr7Bfdu6KGv1J0 fAOW/e0M6D/XfTQTymO2AhXTb8MDn4/TIHRaW9wiIE447KJpvukEE6pyiUMz4yzJDxAH5PBJw3 gRDsP+9D2juftzziciy6890yDut/bIDCMnclsBjJEc6YEWHmYzVEW7wXRsrL1Kk9FPN592iPTe 4VJNqoh9l33uTAxj6ql69aA5pTDVLjeTpxsJRpwUCFyI4D1XGzP+Pk3PYKwG6viQ/7ivIpO9Pv UrXbhWQqG1YgGepVRho2c/yt X-IPAS-Result: =?us-ascii?q?A0C2AADefw9jkAWW5oRaFgUBAQEBAQEBAQUBAQESAQEBA?= =?us-ascii?q?wMBAQFAgU+CJIEBVy4EC0WEToh+iBEDgROdbAsBAwENNwkCBAEBhQcChGQCH?= =?us-ascii?q?QYGNBMBAgQBAQEBAwIDAQEBAQEBAwEBBQEBAQIBAQIEBAETAQEBAQEBFgkeE?= =?us-ascii?q?A4FL2R0gU+BegYDATANgjUpAYNjAQEBAQIBIwQZAQE3AQQLCwwMAgIYDgICV?= =?us-ascii?q?wYTgn0Bgn0lAxCpD3p/MoEBgggBAQaHaQmBESyQFiccgg2BFScPDYIwNz6CY?= =?us-ascii?q?gQYgUaDVjeCLpc2OAMJBAcFLB5CAwsfDhY0GgMUAwUYDAcDGQ8jDQ0EFgcMA?= =?us-ascii?q?wMFJQMCAhsHAgIDAgYVBQICNRg4CAQIBCskDwUCBy8FBC8CHgQFBhEIAhYCB?= =?us-ascii?q?gQEBAQVAhAIAggmFwcTMxkBBTInEAkhHA4aDQUGEwMgbQUHPg8oMjU5Kx0bC?= =?us-ascii?q?oESKigVAwQEAwIGEwMDIgIQLDEUBikTEi0HK3UJAgMiaAUDAwQoLAMJQAcoJ?= =?us-ascii?q?jwFBVk6AQQDAxAiPQYDCQMCJ118liSDCgc3ASBxTaFsjUyTHIIdgT+EJIcHl?= =?us-ascii?q?H8uhUaRLpICHZZqjTmVWYRPgXgjgVtNJBQ7KgGCPAk1EAECAQEBDQECAQEDA?= =?us-ascii?q?QIBAgEIAQECAY4cGYQMN1SJIj80AgEBATYCBgEKAQEDCYVGhQwBAQ?= IronPort-PHdr: A9a23:FOMTrRwF9ns1UwXXCzKXw1BlVkEcU1XcAAcZ59Idhq5Udez7ptK+Z heZv6UzxwGSFazgqNt8w9LMtK7hXWFSqb2gi1slNKJ2ahkelM8NlBYhCsPWQWfyLfrtcjBoV J8aDAwt8H60K1VaF9jjbFPOvHKy8SQSGhLiPgZpO+j5AIHfg9q52uyo5ZHeYARFiDW8bL58M R67sRjfus4KjIV4N60/0AHJonxGe+RXwWNnO1eelAvi68mz4ZBu7T1et+ou+MBcX6r6eb84T aFDAzQ9L281/szrugLdQgaJ+3ART38ZkhtMAwjC8RH6QpL8uTb0u+ZhxCWXO9D9QKsqUjq+8 ahkVB7oiD8GNzEn9mHXltdwh79frB64uhBz35LYbISTOfFjfK3SYMkaSHJdUcleSiJPAoGzY YURAuQOPuhYoZfzqVwJrRalGQmsHebvxiNIhnPq36A31fkqHwHc3AwnGtIDqG7ao8vpNKgMS +C+0bfGzTXCb/xI3Dfy8o7IchY8qvyLQbJwccvRxlcqFwzfiFWQr5foPzKT1uQDtGib9e9gW vizi24mqAF9uCWvxsEtioXQiIIV0E7L9SRiz4YoP924R1R3bsO6H5ZJsSyRKoR5TN84TW5yp CY61qMJuYS9fCUS1pkqyB3SZviDfoWL4x/uVeifLCp3iXxqe7+zmxe//EuvxOD/SMW50ldHo zdEn9fCtH0D2ADe58mJR/dg/0qtxzCC3B3d5OFDJEA7j6vbK5g5z74ojZoTrF7PETHrl0Xrl KOWd0Mk+vKp6+v9eLnmqIWcOolpgQ/9KqQjgtGzDOomPgQUQWSW9/iw2Kf+8UD5XLlGlP07n rHEvJ3UKskXvKC0DxVI3oo/9RqzFSqq3doekHIaNlxKYgiHgJLsO1zWIPD3E/O/g1O0nTdww vDGIqXhDovXInjClrfhc7F961RZyAUp0dBf5pFUBqscIPL1W0/9rdLYDgUnPAy12OnnFc991 owEVW2SHKCVKKLSsVmW6eIzO+SAeYEYtCjnJ/Q76fPikWU1lUIdcKW1x5caaGi0HvF8LEWYZ XrsjM0BEWAPvgcmUOzqiFyCXiBWZ3moWaI84Co2CIOgDYfNQYCtmrmB0z2nHp1XZWBKEE2ME XHpd4mdVfcMcjydIs56nTwZT7ihRJUt2gywuwPizbpoNfLb+jcEupL7yNh1++rTmAks+TBsF cSSz3mNT31onmMPXzI20rh/oUthylef0Kh3neZYGMdS5vNIVwc1LoTcwPZgB9DzXALBZNaJR 0y8TtWoGzE9VsgxzMMWY0ZhB9WiiQjO0DawDL8Qk7yHHZg08qPH33jtPMt90HbH1Kw5j1Y8W MdPNGumhrR+9wfJHYLJnV+ZxO6WcvE12iLX+W6YhVCJp1pSXRR/GfHfWmsEbEbMovz8/kKHV KC1T7M9PV0S59SFL/5yZ8Hklx16RPbuPd3YZSrlh2exCBOBwLWkbYzkfH8Y1TncCw4ZlQFW8 2yLNAIjHCjnr2+IX28mLk7mf065qbo2k3i8VEJhiljSNyWJtpKw8x8R3rmHTu8Lm6kDoGEno il1G1C025TXDcCBrkxvZvYUessztXFA02+RrAlhJtq4Nak3ml4ffgF+uUXG1hN5DZ9FmNQrr zU3ygs3J7iV0VlcbTze0Z2jcqbPJDzU+xaiI7XTxkmY1d+X/qkV7/Ftt1XisQSgEEwK8nNp1 MNQ2med5dPXCgtXX4j8U0wq7Rc8q7yJKjIl6dby0nthebKxrieE298tA749zQ28et5ELK6eP BT3D9VAQcmoJuswnlG1bxFCIeZTsaAuMsKsauGJnqKmVAp5tBShi2kPoIV000bXsjF5VvaNx JEdhfeRwgqAUT74ylanqMH+345eN3kUGSKkxC7oCZQ0BOU6dJsXCWqoP8y8x8lvz5/rVXlC8 Ve/BlQAkMa3cBuWZlb50EVez0MS6XCgnCK5yXRznVRL5uKD3C3Dxu3kcjIGPGBMXmxrkVbvZ 5WyjpUURkWpZRUzm12p6AeyxqRWorh+M3iGWV1BLE2UZylpVqq9sKbHYtYaschy938MCKLlP AjcF+2YwVNSyS7oEmpAySpucjirvs68hBlmkCeGK241qnPFeMZ2zBOZ5drGRPcX0CBVIUsww TTRGFW4OMGkuNuOkJKW+Py+Vm+kX5tVWSjtw4SasSKn5G4sHBu+2v6pl9ztDBI1lyP2nYoPN 22AvFPnb4/n2r7ve/5nf0RtDVn6w8t8FIZkl4IshZJWxH4bw5uP8HsNjH38d9lWk/GbDjJFV XsAxNjb5xLg0UtoIyeSxo73YX6ax9Noe9iwZm5+NjsVycdMBe/U6bVFmXAwuV+ktUfKZuA7m D4ByPwo4XpcgucTuQNrwD/PSrYVVVJVOyDhjXHqp5i3sblXaWCzcLOxyFs2nNavC6uHqx1dX 3Cxc4krHCt55MFyeFzW13i75obhcdjWJdUd03/c2wvAjuVQIZQ3vvsMiy19PGvhvH5j1ug6y BJ00JCwoZKIbWlgveq4DhNeKjzpdpYW8zDpg7xZm5XzvcjnFZFgFzMXGZrwGKvzSnRI7qyhb lvWVmBvzxXTUaDSFgKe9kp8+nfGEpTwcmqSOGFc1tJ6Ah+UOE1YhgkQGjQ8hJ8wUA6wl6mDO A904C4c4lngp15C0OVtYlPjUmbSoQ6ubB81TpaYNh9f8gBBoVrTMImQ9O9yFTxC8dutoUbeT w7TLxQNFmwPVkGeUhr/Prij4NDG9cCZAOS5Nf7HfbSN7/FYVrKG35+u2JZ88HCAO4/cWxsqR +1+0U1FU3djHs3fkDhaUC0bmRXGaMuDrQu98Cl6xiym2NLsXg+npY6GCr8JdM5q5wjzmqCbc eiZmCd+Lz9ckJIK337BjrYFjhYUjGl1ej+hHK5l12aFRb/MmqJREx8Qaj9ifMpO4aUm2wBRO Mndwtrr3798h/QxBh9LT1vk0s2uYMULJSm6OjalTA6TM6+aIDTQ38ztSbi5VaUKyuRSuRqqv D+HEkylIzKC0jfzWhGlLPtDyi2WfVRftIy7bhdxGD3jQdbhOXjZeJd8iTw7x6Fxh2ufbDVGd 2InKwUU8+XWsHA94L03AWFK43t7IPPRni+Y67KdMZMKqb5wBTwyketG4XM8wr8T7SdeRfUzl jGBy7wm61ygjOSLzSJqFRRUrTMezp6LvEhnMKPf3phGV3He+RsR7GbWFhIL4tV/B9zlprpfj NTC3vGWSn8K45fP8M0QCtKBYtqAK2YkOAH1FST8Fw4ZVWTtNGfRgFZYme2T9TuIqJl/pILhm ZATULAdWFF/RZZ4Qgx1WdcFJplwRDYtl7WW2dUJ6XSJpx7UXMxGv5rDW5p64N30LSqB1/9FY RUP27bxMYUQcJD92glscFR7lpnQFAzcUIIVysWORg4yrkJX9XFiT251xkTkLw237X4ZCOS72 BI72FMWiQEF9THi5E0yL0bLp20tlkh0l8/ogDqMajG3IKriBelr IronPort-Data: A9a23:uzIUmquP+KVxdW6Dua6tPoJAwefnVF1bMUV32f8akzHdYApBsoF/q tZmKWHXa/3fZmL1KNlxaonioBkBvJXcy9diTldt+y80QipEgMeUXt7xwmXYb3rDdJWbJK5Ex 5xDMYeYdJhcolv0/ErF3m3J9CEkvU2wbuOgTraCYEidfCc8IMsboUsLd9UR38g52rBVPyvX4 Ymo+52EYQf/s9JJGjt8B5yr+EsHUMva42twUmwWPZina3eD/5W9JMt3yZCZdxMUcKEMdgKJb 7qrIIWCw4/s10xF5uVJPVrMWhZirrb6ZWBig5fNMkSoqkAqSicais7XOBeAAKtao23hojx/9 DlCncTgGBoRGoPMo8syfx0CGiw5IvdWp4aSdBBTseTLp6HHW2Dp3+00SkAwM4oC/+9rAGII6 PoZbT4XYxGJmvi5hr62IgVurp14do+xZ9tZ4yw4i2yx4fUOGfgvR43W5d5V2T42gOhPG/jZf c8QdTtsKgnGYlhBIFoWAo8kk6GkixETdhUC8g/O//psvAA/yiRX9rH/KvfHQuCXYsNZsxmSj GHLpGTmV0Ry2Nu3kmbbrij13ocjhxjTVpoVCKG5++RCklyWzHYaThwQT1qy5/ej4ma1Utdbb kgV4TYGtrk37EXtT9/nXhT+rmTsg/IHc8FVD/VgrgCLxK3O5g+FB2tCUzhALdI8uc48WCYlk FOE9z/0OdBxmOXFGG+l0pmUlhydFSxPJGJFenUUEjJQtrEPv7oPph7IS99iFou8gdv0BSz8z li2kcQuu1kApZJUhvTjojgrlxrz9sWWHmbZ8y2KNl9J+D+Vc6aJSuREA3D19/tBJpuDQRGAu TAugcWf9+8HEPlhfwTSEbxURtlFC96vOTHRhxtQAoM96zmo8XO5cuhtDNxWP0J1KpxCeDnnZ 1XWsB9Q59lOOnrvY7V6YoisEctswaWI+TXZuhL8MYEmjntZLVHvEMRSiai4gz+FfK8EzfFXB HtjWZzwZUv28Iw+pNZMe88T0KUw2gc1zn7JSJbwwnyPiOTAPS7FFe1eagPWNIjVCZ9oRi2Lo 76z0OPUm31ivBHWPHm/HXM7dwhbcCNlXfgaVeQOLr/ZeWKK513N+9eKne19IdU990ikvu3F+ m6gVwdFzlvhiGfcKBmbInZudKzoR5UXkJ7IFXNEALpc4FB6OdzHxP5GJ/MfIOd7nMQ+k68cZ 6deIa2oXK8QIgkrDhxBMfERWqQ5Lk/67e9PVgL5CAUCk2lIHFSSp4e8JVO3rkHjzEOf7KMDn lFp7SuDKbJreuioJJy+hCuHwwzjsH4Dtvh1WkeUcNBfdF+2rtprLSL2lPo+P8APbwjFx36Uz QuXCwoCqq/BrtZtotXOgKmFqaavEvd/RxYLQTOEsOzubSSKrHC+xYJgUfqTeWGPXWz5z6yue OFJwqyuK/YAhltL79JxHu8zn6Iz7tfivZFAyQFgECmZZlinEOk+cHiA085Vs6RRx7wfpA23H 0yV99hQJK+Gfs/oSQZDKA0gZ+WF9PcVhjiLsaVrehqnvncv8ePeA0tIPhSKhChMF5dPMdsok bU7pcobyw2jkR57YN+Jgxdd+3mIMnFdAb4ssYsXAdOzhwcmlgNCbJjbBnOk6Z2DcY4WYFIvP ifOwqvEibNGw0Pecnl1CH7MmORHiJUEpQpFilMPfgzblt3Aj/4x/RtQ7TVuElULlEoaiborN zg5LVBxKIWP4yxs2ppJUVesLB5MWU+C8UvrxlpXyGCAFxu0VnbAJXEWMPqW+BxL6HpVezVWo OOCxGD+XWq4dc39xHBoC1Vgt+S5C913+ArYncm7HsfDAp87JDT/j66keHAH7RfqWJtjiErCr Ohs3eBxdayiaX9O+fJmUdHC2ORCUg2AKUxDXeplovEDE1bcTy6/hGqVIEerd8ITe/GTqR2kC 9ZjL95kXgil0HrctSgSAKMBLteYRhLyCAburl8qGYIHj1dbhiFsrIqKsCn4imgxRtxykMV7N 4XQMjyYH22amGFb3WPAxCWB1qxUfvFcDDAQHsjsmAnKK37HmOBqf0Yo17KovnbTLQ1muhyOs QLJerXZieBvoWipc00ADY0bbzhZ6rrPuCCg8Qa9tM5LZM/OMoHTsQJQpEPqPg5LJ7RXV9kfe XFhdjLo9ButgYvamFw1V3VM+2elKClysCdq3hrLEURn IronPort-HdrOrdr: A9a23:z+ymBqznm+diWc54eaT5KrPwFb1zdoMgy1knxilNoNJuA6+lfq eV7ZYmPH7P5Qr5PUtKpTnuAsm9qB/nm6KdpLNxAV7dZniChILYFu1fBFvZskTd8kTFn4Y26U 4jSdkbNDSaNzdHZKjBkW6F+q4bsb+6zJw= X-IronPort-Anti-Spam-Filtered: true X-IronPort-AV: E=Sophos;i="5.93,278,1654552800"; d="scan'208";a="22532837" X-MGA-submission: =?us-ascii?q?MDFYScrUyBzZrIpO/niE3+hR8/GlvVFFFeORNq?= =?us-ascii?q?M+qNmwaOJOiNLzer8KCvQPZ8vPwV+V0u5VvGXX5x1mcJOkK8Q7X4s9yh?= =?us-ascii?q?vOyyEALeZuXQvL2PtD1qcSQ9nk/O5Pfai7GX41ekpJhtxpBKH/Ef09DW?= =?us-ascii?q?g7uhMBBGuDuDGpyKmo7IUy9g=3D=3D?= Received: from smtp2.informatik.uni-freiburg.de ([132.230.150.5]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/ECDHE-RSA-AES256-GCM-SHA384; 31 Aug 2022 17:40:52 +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=KOhsNI5WaDVcmQTby9TyjK4+JqwlY7TBNZDQ856IbRo=; b=YUqTvQbinXfeS1rVEJ/EoDewUJ Bkt4IlSH1i9ssziZtcUsAF6+33rpftjgnKlJ7Ws8vjpKTJwc9EhGhcW6hBwpe+j1weGIMRxQXrAVP WJXrK8iXRfDIl+SMC1lZB3MvT2GysWMiQH3AVzm0XdusCto22M1EP//AuZClsU+TEOAaXLyinBrAM 0yNdR2MtNVnFdWl5UjuKBKRkIfKOnhGPQBn3dpFmWyQcFUHUkkYdcWFduP+mv/3YgKRorDzMoSWnC bw9YN45yumOccW8y3YUgSYTacUwwxfcbIVU/owf3wEqDYOeCaOMBBHxEQa1TONiXwqEGtcwcxa6iE FeVjcX8g==; 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 1oTPve-0006IZ-TE; Wed, 31 Aug 2022 17:40:51 +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: <9C63A771-E4AD-42E4-A889-56CB1FFB563E@mpi-sws.org> Date: Wed, 31 Aug 2022 17:40:50 +0200 Cc: Peter Thiemann , =?utf-8?Q?Fran=C3=A7ois_Pottier?= , 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> <9C63A771-E4AD-42E4-A889-56CB1FFB563E@mpi-sws.org> To: Andreas Rossberg X-Mailer: Apple Mail (2.3696.120.41.1.1) Organization: Universitaet Freiburg, Institut f. Informatik Subject: Re: [Caml-list] coinductive data types Hi Andreas, > On 31. Aug 2022, at 11:41, Andreas Rossberg = wrote: >=20 > Hi Peter, >=20 > yes, I think they are different things. With (nominal) algebraic data = types: >=20 > type peano =3D Z | S of peano > type nat =3D Z | S of nat > let f (x : peano) : nat =3D x -- type error >=20 > But with iso-recursive types: >=20 > type peano =3D mu peano. 1 + peano > type nat =3D mu nat. 1 + nat > let f (x : peano) : nat =3D x -- ok Sure! >=20 > Of course, it is merely a pragmatic choice that ML (and many other = languages) treats algebraic types as nominal. It could just as well = treat them as structural. In a sense, OCaml=E2=80=99s polymorphic = variants behave more iso-recursively than its data types (at least until = you activate --rectypes and opt into equi-recursive semantics). With "pragmatic" you mean that type checking gets more efficient or do = you have some other pragmatic aspects in mind? IIRC, polymorphic variants are just (open) sum types, which admit = equi-recursion. Viz the behavior of the degenerate, one-armed = polymorphic variant to "implement" iso-recursion: # let rec m =3D `Fold m;; val m : [> `Fold of 'a ] as 'a =3D `Fold # let unfold (`Fold v) =3D v;; val unfold : [< `Fold of 'a ] -> 'a =3D >=20 > FWIW, some old notes by Crary et al. [1] discuss this very choice, and = how it interferes with modules. Moreover, based on their observations, = the Harper/Stone semantics for SML actually models data type definitions = as opaque abstract types (modules, really) that are merely _implemented_ = by an iso-recursive type. That is both to capture their nominal = (generative) semantics, but also to be able to express partial = abstraction of mutually recursive types: >=20 > module type S =3D > sig > type t > type u =3D U of t > end >=20 > module M : S =3D > struct > type t =3D T of u > and u =3D U of t > end >=20 > This is not expressible directly with iso-recursion, as explained in = [1]. Thanks for the pointer to this gem! Best -Peter >=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 > 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