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 3DCF4E0128 for ; Wed, 31 Aug 2022 18:44:41 +0200 (CEST) Authentication-Results: mail3-smtp-sop.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 (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of rossberg@mpi-sws.org) identity=pra; client-ip=139.19.86.40; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="rossberg@mpi-sws.org"; x-sender="rossberg@mpi-sws.org"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.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=mail3-smtp-sop.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 (mail3-smtp-sop.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=mail3-smtp-sop.national.inria.fr; envelope-from="rossberg@mpi-sws.org"; x-sender="postmaster@juno.mpi-klsb.mpg.de"; x-conformance=sidf_compatible IronPort-SDR: 5z4JXhLrIz4Uqz3u6t5d6XN1dLnEtcMYELOdlZrn3byBx53e2tIfdcmbesrVUyAIL7DQ9FPi22 bD4IeZfP2sgOncty6mVprT/EHtvHmGEMqTWXD12yVTaRY9vrhM6qr/7kb7QA30ctJjwH6bekvl lvgyx4KY92V8or3oiNAFiUETD3qBuC/cCtwt/k/2eyXfnkd7CEFesfkNUc6BKxb1BdDTxehp2Y I8aab4oLuuu9Tt9bAUD02EMnKejTli20Vvy0bdzKSnJAAn65GpNbn8pvz626GmiH34WHYAh7Y9 vlZ440DvJ47wbwGPSSnT24V8 X-IPAS-Result: =?us-ascii?q?A0DXAABTjw9jmChWE4taFgYBAQEBAQEHAQESAQEEBAEBg?= =?us-ascii?q?g+BIYEDgQFYLQQLRYROkQ8DgROdbAsBAwENNwgBAgQBAYUHAoRkAh0HAQQ0E?= =?us-ascii?q?wECBAEBAQEDAgMBAQEBAQEDAQEFAQEBAgEBAgQEARMBAQEBAQEBARQJGQUQD?= =?us-ascii?q?gU8ZGQDgUwDgXoGBDANgjUpAYNjAQEBAQIBIwQZAQE3AQQLCwwMHAQBCQICV?= =?us-ascii?q?wYTgn0Bgn0lAwQMqRJ6fzKBAYIIAQEGgmCFCQmBPYg9AYdYJxyCDYEVJxyCM?= =?us-ascii?q?Dc+gmIEGIFzgyk3gi6XMAc3AwkEBwUsHkIDCx8OFjQaAxQDBRgMBwMZDyMND?= =?us-ascii?q?QQWBwwDAwUlAwICGwcCAgMCBhUFAgI1GDgIBAgEKyQPBQIHLwUELwIeBAUGE?= =?us-ascii?q?QgCFgIGBAQEBBUCEAgCCCYXBxMzGQEFWRAJIRwOGg0FBhMDIG0FBz4PKDI1O?= =?us-ascii?q?SsdGwqBEiooFQMEBAMCBhMDAyICECwxFAYpExItByt1CQIDImgFAwMEKCwDC?= =?us-ascii?q?SEfBygmPAUFWToBBAMDECI9BgMJAwInXXyWJIMKBAM3ASBxTSVyoFWNTJMcg?= =?us-ascii?q?1yEJIcHlS2FRpEuBpF8HZZqjTmVWYRPgXgjgVtNMAg7KgGCPAk1EAECAQINA?= =?us-ascii?q?QICAwECAQIBCAEBAgGOHBmEQ1SDVoVMQDMCAQEBNgIGAQoBAQMJhUYBAQGFC?= =?us-ascii?q?QEB?= IronPort-PHdr: A9a23:cApj1BSByg+VQXztjEqS0om+rdpsoh6VAWYlg6HPa5pwe6iut67vI FbYra00ygOTBsOBu6wP1LeempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yN s1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffQtFiCCjbb5xL Ri6ogfcu8kLioZ+N6g9zQfErGFVcOpM32NoIlyTnxf45siu+ZNo7jpdtfE8+cNeSKv2Z6s3Q 6BWAzQgKGA1+dbktQLfQguV53sTSXsZnxxVCAXY9h76X5Pxsizntuph3SSRIMP7QawoVTmk8 qxmUwHjhjsZODEl8WHXks1wg7xdoBK9vBx03orYbJiIOPZiYq/ReNUXTndDUMlMTSxMGp+zY IQSAeQBP+lWoZfwqVgArRWgAgehH/ngxiNNhnLs3a02z+YsHAfb1wIgBdIOt3HUoc3pOacUT O+11rfHwi/Yb/hLxTn975PIcgs6rv6SR7JwftfaxE41FwPClVWQspfqMC2P1uQCqGWb6vJgV eO2h248pQBxuSKjxsA2ionGn48YzE3P+iplzogvP9K4VFJ7bsC+EJtWryyXNoV7T8cgTmxqp Co3yL0ItJ6lcCUKypkqxQDTZfKIfYSW4R/uV+KcLDVmiXxrdryyhxi//Eekx+DiSsS50FhHo yxYmdfCsXAN0gbc6smBSvZl5kehwiuP2xrN5e5ZPEA4javbK5g7wr4xjJUfq0rDHjXwlU7rj 6GWbl0p9vWm5unjeLnqu5uRO5V3hwz/KKgjldCzDfwmPgQTQWSX4+qx2KH58UD3QbhGlOA6n 6bavZ3cOM8VvLS2AxVP3YYm8xu/Dymp0NAfnXQfLlJFZRSHj4/zN1HLOPD4DO6zg1eokDdw3 P/KJLjhAo3CLnTZjbjuY65x609ayAUt0dBS/49YB78FLf7pR0P8sMbUAxw4PgCuzOvrFM1x1 oYEVmKOBq+ZPrnSsViN5u83OemMY5QVuC3mJPc7/f7ugmQ0mVoFfamoxJcXc365Hu98L0Wee 3rsjc8NEWERsQUmVuzllEWCUSJPZ3a1R68w+Ck3CJi6AofbWoCtnLuB0T+1Hp1OYWBGFkyME Xb2eIWeQPoNaSOSIsp6nTweT7etUY4h1Re0tA/70bVrNOTU+jcAuZL5yNd1//HTlQ019TFsE 8uSyWSNT2VtkmMMRj82x7x/rFdmylaD1Kh4m+ZXGcZS5/NPSAc6NITTw/Z0C9DoCUr9eYKxR UqrWJ2aATA8S9s3xZdaf0Z8FtCriBbr3iykBKUQnqCKB9op9KOZ0WL8Jsxg0XmA2KR33Hc8R c4aHGuqnKN27EDpAJXSmUiDmO7+b6MHxyTA7miryHKP+VpHS0h3S6qTDiNXXVffsdmsvhCKd LSpE7lyd1IZkaZqS4NPY9zt1hBdQev7fc/ZeyS3knuxAhCBwvWNapDrciMTxnaVE1AKxiYU+ 3vOLg0iHmG5uWuLFjt1DljieUzE9PF/7WikVQkz1Q7ZJ1Z52e+N8wUOzeeZV+tV27sFvCk7r DAhBlGmxNjbEdWoohJgOb5DepU6+lgUnXnBuVlbOZqtZ7tnmkZYcwlzuBb20A5rD4xbjcUwh HE3yg00LLqZlVBFbDne2Ij/fLHaQoXr1DaobaOemlTX0dLNv7wK9Ox9sFL7+gegCksl9Xxjl dhTyXqVoJvQXkIUVtrqX0A7+gIfxfmSazQh547SyXxnMLWl+j7E1dUzAeI5yxGmN95BOaKAH QX2HoUUHc+rYOAtnlGoaFoDMoUwvOYuONi9ffac14auJOclhy29y2Nd78E1006B8TZ9Vv+dx 4wMkLmT2gqKUSu5jU/065um39kVI2FMWDbnmk2GTMZLa6Z/fJgGEzKrKsyznZBlgoL1HmVf7 BilDk8H38mgfVyTaUb81EtezxdywzTvlC2mwjhzizxsoLCY2XmE2eP5bxAKIGFjQXFjyEzzO s6zld9QDy3KJ0A50QCo40r33f0RvqNkNGPeW0hgejD3anp9Se23rLXIMKstoNs49C5QVuq7e 1WTTLXw9gAb3y3UFGxb3Dkndjuut/0VhjRCgXmGZDZ2pXvdIoRrwAvHocfbXbhX1yYHQy9xj X/WAEK9Np+n54fcm5DGu+G4H2WvM/8bOTPs1piKuTG0zWhyAFikgOv1ncfoWQQ3yi700dB2W D6A9U2tJNC6kfTkd74/NkBzTEfx8c97Bp1znu5SzNkL1H4Wi4/UtXsLnGHvMMlKjKf3bX4DX zkOkJbe5Ano3lEmL2rcntmoECzMhJs/IYXiMQZ0kmon4stHCbmZ9ulBlCpx+R+jqB7JJON6h nEbwOcv73gTh6cIvhAsx2OTGON3fwEQMCrymhCP9937or9QYTPla7+rz0Bzh9+JCamD5xpDQ zD+YJhoTkoSpo1vdUnB1nH+8NSuYt7LdtgerBK8lg/ByvNKM9Q2jPVA1k8FcSrt+HYizeA8l xln25q36ZOGJ2ta96W8GhdENzfxapBb6nT3gK1ZhMrTw5G3E8ArBGAQRJWxB6HNcnpapbH9O g2JCjF5tnqLBe+VA1qE8Ek/53udE52xPjeSPHhcztF5Tl+YPEMZjA1xPn1yl8w7Cwatgsn5c QJ64isboFvgpV1Ax6phZQH7T3vY4gKwa3I3TIOVah9O4UdO6iK3eYSXvOtrGCVc+duktA3IK WiAbUJNFW5PVkHMDgLhI6Gv+dTate2AB6+9K+DEJ7CWpqpSWpLqjdqmgJNh5DuNOsKJeHx6D rg43lFJG3VhFILVln1YQigT3Uohdua9oxGxsm1yp8G7q7HwXR73oJCIE/1UOMlu/Ba/heGCM fSRjWB3M2QQ0JRE3nLOxLUFuTxawyhzazmgF6gBvi/RXerRnKFQFRsSdyJ0MoNB8as92gBHP cOThMny0/Z0ifs8ClENUlKE+InhfcsRP2S0L0/KHm6JKbKBYzjTwoT0Zbi2D7hIg6NYulz4u DqWFVPiIiXWlzTtUEPKU6kEhyWaMRpC/YClJ082WC66HZS2NFvnaIwS73V+27A/i3LUOHRJN DF9dxgItbiM9WZDhe05HWVd731jJO3CmiCD7uCeJIxF1JkjSilyie9e52w3jrVP6yQRDuZyg zDYo8Rhi1S+k6yU1SEhVwBB4GUu5srDrQB5NKPV+4MVE27D5w4I5H6MBg4ipcZjDZvqo6EVy dzUnuT2MDgE/9+erq5+T4DEbcmANnQmKx/gHjXZWRAEQTCcPmban0VBkfuW+xV9QbA/spmpg 4UVDLhBWw5sfhv7IkZ4GttEJY92GzAgirTdidYHo3az/kG5rCByu4jGE+mNGrPoMjnL1dF5 IronPort-Data: A9a23:UgD1hK++sUiqYASo5A0jDrUDZ3iTJUtcMsCJ2f8bNWPcYEJGY0x3m DNKXTqFPf/bNDT1KN0kb96/o0IOsZTTnddnGgI6/C9EQiMRo6IpJ/zJdxaqZ3v6wu7rFR88s Z1GMrEsCOhuExcwcz/0auCJQUFUjP3OHvymYAL9EngZqTVMEU/Nsjo+3b9i6mJUqYLhWVnV6 Yir+5e31GKNglaYDEpEs8pvlzs05JweiBtA1rDpTa0jUPf2zhH5PbpHTU2DByOQrrp8QoZWc 93+IISRpQs1yfuC5uSNyd4XemVSKlLb0JPnZnB+A8BOiTAazsA+PzpS2Pc0MS9qZzu1c99Z4 5YWrLaZdywSAe7pncUiShBcFxlhBPgTkFPHCSDXXc27zVDAdD3p2/QrD0UtN8sd4ukxDWwmG f4wcWtcKEnSwbLohu7jIgVvrpxLwM3DJoQEoXtt1z7xCO4nBIvcWOPN/9AwMDIY3JoTRqaCO JtxhTxHMzHNTg9mAlEuCrFmo8aZoimveRYDpwfAzUYwyzKKl1UqgOmF3MDuUtKSQtlJn0uCj nDH+m7jC1cbMsaewHyL6BqEjebKmWb/WZkOPKap8+ZjxlyV3G0aThMMPWZXutG7l0i5HddHK gkX/jEk660q+wqnQ7ERQiFUvlav/UUFcfNuONYFqySI65XN6gKdPnc9G2sphMMdiOc6Qjkj1 1msltzvBCByvLD9dZ573unPxd9VEXZPRVLudRPoXiNYuoOy8dpbYgbnH4oySfbdYsjdQ2moq w1muhTSkJ0/oKY2O0iT/03BhHSpvpmMTQou7EPSRm3j4g4RiG+Zi26AtwizARVoddvxory9U J4sxpL2AAcmUMvlqcB1aL9RdIxFHt7cWNEmvXZhHoM66xOm8GO5cIZb7VlWfRk3a5ZUJWWyO RaC5Wu9AaO/2lP1M8ebhKruV6wXIVTIT4i1PhwpRoUfMsguL1HvEN9GOBbOhzmFfLcQfVEXY 87AKJ38XB72+IxrwSeqXOwd3KRjyCck3mjTWJb01BKqzaj2WZJmYehtDbd6VchgtPnsiFyMq 753bpLaoz0CDrGWSnSJoOY7cwtQRVBlXs+eliCiXrPZSuaQMDt/W6a5LHJIU9ENopm5Yc+Tr y3kBh4FkweXaL+uAVziV02PoYjHBf5XxU/X9wR3Vbpx83R8M4up8okFcJ47Iesu+OB5lKcmS uEEPt6fGbJIUDueo2YRapz0rYpDchW3hFvXZXD9OWJlIMJtF17T59vpXgrz7y1SXCC5gs0z/ u+73QTBTJtfGglvVZ6EaP+mw16rk2IaneZ+AxnBLtVJIRy+9ZBrbjfulbkwOc5VcUfPwT6T1 gC3BxYEpLCU+dVtqYOT2vyJ9t77HfF/E0xWG3jgwYy3bSSKrHC+xYJgUfqTeWyPXm3D/qj/N /5eyOvxMaFakVtH79h8HrJswf5s7tfjveUCnAZ5GnKNakyqT7BkOXPA2NFA8KFAn+cLtQyzU 0OJ299bJbTQZJK7SgFMflJ9Y7TRz+wQlxnT8e8xfhfw6hh3y6XZA09cCBm7jiEAfqB+N5kow Lp/tZdOuRC/kBcjLv2PkjtQqzaXNnUFXqh75IsWBpTn1lgixl1YO8SOCDLw59eKc9QJMU0xK HmRnKWEi7kFnhjOdH86FH7s2+tBhM1S6U4QkwJYfwyEyojfm/s6/BxN6jBpHA5b+RVwzLwhM GZcN3pzKPjc5DxvnsVCAj6hQlkTGB2D90Xt4FIVj2mFHVKwX2nAIWBV1TxhJ6zFH7awvwS3/ Y10DE7nTDDtOsTp324xXVVv7fn7Qpp9+2UuXSxh89utR/EHjfjN28dCplbkbzPiGcJ0n1Lc4 +5w846crIXlYDUIrfRT55ayjNwtpdPtGICGafR5/eYSAnqafyu9sdRLx4ZdZesVT8H3HYSE5 wCC6y6Bu9lSFMpDk9zDOZMxHg== IronPort-HdrOrdr: A9a23:7ftBMqsS2yzRnfZnPNmHGQ0y7skDvNV00zEX/kB9WHVpmwKj5q KTdZUguSMc7Qx7ZJhOo6HiBEDtexLhHNtOgbX5Q43SOTUOyVHGEGgK1+KLqVDd8m/Fh4pgPM xbHZSWZueAamSS9fyKhjWQIpIa+uCu1I3tru/Epk0dNj1CWuVa1T5QLiveKUFuQhJabKBJbK a01459nQOJXVlSVM68HXVtZZm7m+H2 X-IronPort-Anti-Spam-Filtered: true X-IronPort-AV: E=Sophos;i="5.93,278,1654552800"; d="scan'208,217";a="22538479" X-MGA-submission: =?us-ascii?q?MDENbfqbfjZzokbU+2+MYYjTdKkkBYaPHeHkjv?= =?us-ascii?q?H2ggZOPlMARFJOrR0YRFZnIZKGxrHlKtEN95lVBZgtfwMf0ZIijF00LN?= =?us-ascii?q?yCllgdByNA+RZQYZ4ZlvCseYrXW2q4BEt2ot+SBf7vrTd1OVibWkeBxV?= =?us-ascii?q?NgtFV4rEo97MogFl1nRLqpnA=3D=3D?= Received: from juno.mpi-klsb.mpg.de ([139.19.86.40]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/ECDHE-RSA-AES256-GCM-SHA384; 31 Aug 2022 18:44:40 +0200 DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=mpi-sws.org ; s=mail201904; h=To:References:Message-Id:Cc:Date:In-Reply-To:From:Subject: Mime-Version:Content-Type:sender:reply-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=BO2tBbxsdydPzhgZ36M36V7u/YZYYrPuIzUGaeyi9YE=; b=pGFvk6XUbrzlkRuD6LuIGKv8Ua o4bJU0J06p2j6xEzBd+fAQmzV9nhwSFDzDja8DmvlXtnRhGzpKaMI3oPejPHqGBPrE1mQ+JZxDlBg sf1sbDqPBj2r1USzFO9AXm4O36lg/FE5YeES3SyjxMwfOIELvQRGkUfxFuFsbzi6akAA=; Received: from max.mpi-klsb.mpg.de ([139.19.86.27]:51344) by juno.mpi-klsb.mpg.de (envelope-from ) with esmtps (TLS1.3:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.92) id 1oTQpM-00053Z-45; Wed, 31 Aug 2022 18:44:39 +0200 Received: from [212.30.36.148] (port=62965 helo=smtpclient.apple) by max (envelope-from ) with esmtpsa (TLS1.2:ECDHE_SECP256R1__RSA_SHA256__AES_256_GCM:256) (Exim 4.94.2) id 1oTQpL-00BtWw-EC; Wed, 31 Aug 2022 18:44:31 +0200 Content-Type: multipart/alternative; boundary="Apple-Mail=_7191D293-E417-4EDB-AF69-8B5DB42A2684" Mime-Version: 1.0 (Mac OS X Mail 16.0 \(3696.120.41.1.1\)) From: Andreas Rossberg In-Reply-To: Date: Wed, 31 Aug 2022 18:44:29 +0200 Cc: =?utf-8?Q?Fran=C3=A7ois_Pottier?= , caml-list@inria.fr Message-Id: <60EF29A4-60B5-49DB-9CE6-7DB69AE9A608@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> To: Peter Thiemann X-Mailer: Apple Mail (2.3696.120.41.1.1) X-RSPAMD-Score: 0.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: RCPT_COUNT_THREE(0.00) Symbol: MIME_GOOD(-0.10) Symbol: TO_MATCH_ENVRCPT_ALL(0.00) Symbol: DMARC_NA(0.00) Symbol: TO_DN_SOME(0.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: 60EF29A4-60B5-49DB-9CE6-7DB69AE9A608@mpi-sws.org X-RSPAMD-Bar: / Subject: Re: [Caml-list] coinductive data types --Apple-Mail=_7191D293-E417-4EDB-AF69-8B5DB42A2684 Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 > On 31. 8. 2022, at 17:40, Peter Thiemann = wrote: >=20 > Hi Andreas, >=20 >> 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 >=20 > Sure! >=20 >>=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). >=20 > With "pragmatic" you mean that type checking gets more efficient or do = you have some other pragmatic aspects in mind? It probably also is easier to explain to many programmers and produces = more readable error messages. > 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: >=20 > # 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 Yes, I think you are right that equi-recursion is still observable, but = this may be the wrong example. I think it merely shows that OCaml=E2=80=99= s let-rec is a more general fixpoint, but that also works with ordinary = data types: type t =3D Fold of t let rec m =3D Fold m let unfold (Fold v) =3D v But the following example should reveal the underlying equi-recursive = semantics: # let f (x : [`Foo of [`Foo of 'a]] as =E2=80=98a) : [`Foo of 'b] as 'b = =3D x;; val f : ([ `Foo of 'a ] as 'a) -> 'a =3D So yeah, strike my remark about polymorphic variants. :) >=20 >=20 >>=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]. >=20 > Thanks for the pointer to this gem! Just to clarify and expand on my earlier remark, the way the = Harper/Stone semantics eventually solved both problems was not by = adopting =E2=80=9CShao=E2=80=99s equation=E2=80=9D as predicted in those = notes (which would require coinductive type equivalence, throwing a = major advantage of iso-recursion out the window). Instead, they model = the definition type t =3D A | B of t as (the equivalent of) open ( struct type t =3D mu t. 1 + t let A =3D fold (inl ()) let B x =3D fold (inr x) let case_t x f g =3D match x with inl y -> f y | inr z -> g z end : sig type t val A : t val B : t -> t val case_t : t -> (unit -> 'a) -> (t -> 'a) -> =E2=80=98a end ) This explains datatypes as a combination of iso-recursion and the = existing semantics for type abstraction (which could in turn be = explained as existential quantification, of course :) ). Cheers, /Andreas >=20 > Best > -Peter >=20 >=20 >>=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/ --Apple-Mail=_7191D293-E417-4EDB-AF69-8B5DB42A2684 Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8

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

Hi Andreas,

On 31. Aug 2022, at 11:41, Andreas = Rossberg <rossberg@mpi-sws.org> wrote:

Hi Peter,

yes, I think they are = different things. With (nominal) algebraic data types:

 type peano =3D Z | S of peano
 type = nat =3D Z | S of nat
 let f (x : peano) : nat =3D x =   -- type error

But with = iso-recursive types:

 type peano =3D = mu peano. 1 + peano
 type nat =3D mu nat. 1 + nat
 let f (x : peano) : nat =3D x   -- ok

Sure!


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?

It probably also = is easier to explain to many programmers and produces more readable = error messages.

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 <cycle>
# let unfold (`Fold v) =3D = v;;
val unfold : = [< `Fold of 'a ] -> 'a =3D <fun>

Yes, I = think you are right that equi-recursion is still observable, but this = may be the wrong example. I think it merely shows that OCaml=E2=80=99= s let-rec is a more general fixpoint, but that = also works with ordinary data types:

type t =3D Fold of t
let rec m =3D Fold = m
let unfold (Fold v) =3D v

But the following example should reveal the = underlying equi-recursive semantics:

#= let f (x : [`Foo of [`Foo of 'a]] as =E2=80=98a) : [`Foo of 'b] as 'b =3D= x;;
val f : ([ `Foo of 'a ] as 'a) -> 'a =3D = <fun>

So yeah, strike my = remark about polymorphic variants. :)





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:

module type S = =3D
sig
 type t
 type = u =3D U of t
end

module M : S = =3D
struct
 type t =3D T of u
 and u =3D U of t
end

This is not expressible directly with iso-recursion, as = explained in [1].

Thanks for the pointer to this gem!

Just to clarify = and expand on my earlier remark, the way the Harper/Stone semantics = eventually solved both problems was not by adopting =E2=80=9CShao=E2=80=99= s equation=E2=80=9D as predicted in those notes (which would require = coinductive type equivalence, throwing a major advantage of = iso-recursion out the window). Instead, they model the = definition

  type t =3D A | B = of t

as (the equivalent = of)

  open (
    = struct
      type t =3D mu t. 1 + t
    =   let A =3D fold (inl ())
      let B x =3D fold (inr = x)
      let case_t x f g =3D match x with inl y -> = f y | inr z -> g z
    end
  : = sig
      type t
      = val A : t
      val B : t -> = t
      val case_t : t -> (unit -> 'a) = -> (t -> 'a) -> =E2=80=98a
    = end
  )

This explains = datatypes as a combination of iso-recursion and the existing semantics = for type abstraction (which could in turn be explained as existential = quantification, of course :) ).

Cheers,
/Andreas



Best
-Peter



(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.)

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=A7ois Pottier
francois.pottier@inria.fr
http://cambium.inria.fr/~fpottier/

= --Apple-Mail=_7191D293-E417-4EDB-AF69-8B5DB42A2684--