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 54944E0128 for ; Wed, 31 Aug 2022 11:42:06 +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: qO7qYlfWe0M+SlGaxzg77MOkYD77+6bZGrXum6bOr9eic8oZBBiBpej6jcWKZ9SyVsJINHzys/ 0TVf9Eao1AHmCHwYdcwau7jkN101CuXli2WqGvPxK5XqF8v7CaVrvSZtnNTcaChoNOdF9kImiJ t0Bn6UBerta/lq21F/LvEsM5mQt+SxyZrCV/I64nLoXDXa/d2VfzebgR5y5fuC7rKjklT1ctrw 0WYXCgk4AwACasXVZZoPWKuv11rmjAoIM5WKHFabxb2v1v9DwW7/fvsSZ0y1FJtowdrynPDVZP bccE50gLrn403FfOpdW7LSQI X-IPAS-Result: =?us-ascii?q?A0DWAACALA9jmChWE4taFgYBAQEBAQEHAQESAQEEBAEBg?= =?us-ascii?q?g+CJIEBWC0EC0WEToh+iBEDgROdbAsBAwENNwgBAgQBAYUHAoRkAh0HAQQ0E?= =?us-ascii?q?wECBAEBAQEDAgMBAQEBAQEDAQEFAQEBAgEBAgQEARMBAQEBAQEBARQJGQUQD?= =?us-ascii?q?gU8ZGQDgUwDgXoGBDANgjUpAYNjAQEBAQIBIx0BATcBBAsLDAwcDgICVwYTg?= =?us-ascii?q?n0Bgn0lAwQMqAx6gTGBAYIIAQEGgmCFCQmBPYg7AYdWJxyCDYEVJxyCMDc+g?= =?us-ascii?q?mIEGIFzgyk3gi6XLgc3AwkEBwUsHkIDCx8OFjQaAxQDBRgMBwMZDyMNDQQWB?= =?us-ascii?q?wwDAwUlAwICGwcCAgMCBhUFAgI1GDgIBAgEKyQPBQIHLwUELwIeBAUGEQgCF?= =?us-ascii?q?gIGBAQEBBUCEAgCCCYXBxMzGQEFWRAJIRwOGg0FBhMDIG0FBz4PKDI1OSsdG?= =?us-ascii?q?wqBEiooFQMEBAMCBhMDAyICECwxFAYpExItByt1CQIDImgFAwMEKCwDCSEfB?= =?us-ascii?q?ygmPAUFWToBBAMDECI9BgMJAwInXXyWFIMKBzcBIIE+oWygaINchCSHB5Uth?= =?us-ascii?q?UaRLgaRfB2Wao05lVmET4F4I4FbTTAIOyoBgjwJNRABAgECDQECAgMBAgECA?= =?us-ascii?q?QgBAQIBjhwZhENUg1aFTEAzAgEBATYCBgEKAQEDCYVGAQEBhQkBAQ?= IronPort-PHdr: A9a23:JV5EtBFty4218eZBH4RAO51Gf4NGhN3EVzX9CrIZgr5DOp6u447ld BSGo6k31xmTDdiQsqIMotGVmpioYXYH75eFvSJKW713fDhBt/8rmRc9CtWOE0zxIa2iRSU7G MNfSA0tpCnjYgBaF8nkelLdvGC54yIMFRXjLwp1Ifn+FpLPg8it2O2+5ZPebx9WiDe+Yb5+I wi6oAbMvcQKnIVuLbo8xAHUqXVSYeRWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2Q rxeFzQmLns65Nb3uhnZTAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v9 LlgRgP2hygbNj456GDXhdJ2jKJHuxKquhhzz5fJbI2JKPZye6XQds4YS2VcRMZcTzBODYyhY YUPDeUPM/hVoYrzp1UQqhWzHhOjCP/qyjJShn/6wa833uI8Gg/GxgwgGNcOvWzIodXzKagSS /66w7PTzT7ec/1W3iz96JPTfR8/u/GMUq97fM3LyUkoDAPFlU6fppL/PzOazekNtnCb7+t5W eK0hW8nsBt9oj+1xscjk4TEgJ8exV/Y+ytj2ok1OcG4R1BhYd6iCJZdti+XOo90T84gX21lu iY0x70YtZO7fiUHyooryRDQZfCZcIWF4RbuWeSPLDl2inxoeLyyihm2/EW+1uDxVse53VBXp SRLldnMs2oC1x3V6sWfUvt95Vqh1SyR2A/O9+FIOUE0lazBK54g2LE8jJQTsV7FEyTrm0v2l Lebelgq9+Ws8ejrf7HrqoWfOoJ1kA3zPbgiltShDeglLAQCRWaW9fim2LDt/ED1WqhGg/I1n 6TfrZvUP94UprSjDA9Qyosj6wiwDzOh0NkAn3kHMVRFeBWdg4jsI1HOIen0DfS7g1S3izhn3 fXGPqXuApnXM3fMjq/tfbd760FC1Ao+1c1T6pxQB70bPf7+XlX9ud/ZAxMjPAG43/7rCNBn2 YMfXWKPDLWZMKTXsVKQ/OIvJPKMZJQOtznjMfgl6OXjjXohmV8cZKWpxpUWaGuiEvRhOUWZb mLggtEaHmgSpAoxUPTqiEGeUT5Uf3u+Qbow5isnB4K+EYfDWoetjaSP3CejGZ1WenxGClGSH nfybIiFWvYMaCeJLc97iDMIT7mhS4k71RGvrgD20bRnLvDM9i0CqZ3jzMR15/HUlRwq6TN7F cGd02WUQ2Fwn2MIXCM20btkoU19z1eDybJ3j+ZZFdxV/fNJUx01OYTSz+xgWJjOXVf5c8uEU h6aQtSrBDg3SJpl398PbkN0HdOKjxbN2DCvCqMUlPqWAp1x/LjR3nLsPck7x3uQh4c7iFxza 81DL2CvneZF8BPIDYPTnA3NjaGxbq4RxiHl8X+CiHGRpwdfSgEmAvaNZmwWekaD9Yex3UjFV bL7TO1/amOpqOaHI6pOMJjyiEleAe3kM5LYan6wnGG5AVCJwKmNZczkYTZVxz3TXW4DlQ1b5 nOaLU4mHC70uWXFFzZjD13HZlvttPJhszW8VEBnhxqSYRhZ3qGusgUQmeTaTvoS2rwevyJ0s TJvB1ywxd3+DsKB4hF+Z+Nbe9xuqExf2zf/sApwdoelM7gkhlMadFFvuFjy0hxsFohauco3q nRsyRJzbKGcy1kHciuXm5z9UlHOAk/1+h3nK6vf21WElc2T5r9K8vMz7VPqoACuEEMmtXRhy dhclXWGtN3MC0IJXJT9X1xSlVAyrqzGYiQ7+4Lf1GF9eaiyvDjY3ts1Bewjgh++dtZbOamAG Uf8CcofT8SpLeUrnRCuYHdmdKhI87UvNc68eNODwK/uJ/l72jW8giUP4Yxw1F6N6zspUvTBj N4Ox/CV2BfCVi+p1Qzw9Jmm39AaI21KTQ/dgWD+CYVcZ7N/Z9MOAGaqeYisw8lmwoTqUDhe/ UKiAFUP3ImofwCTZhrzx141twxfrHq5lC+/1zExnSsuq//VxivV2O7vbhUvP3ZKAXJ9lhHrO 4f+3LV4FAC4KhMkkheo/xOw3a9Av65yNWb7RF9JOjPpNCdlSKT65d/gK4ZfrZgvtytQSuG1Z 1uXH6X8rxUt2CTmB2JCxTo/ellGo73BlgdhwCKYJXd39j/CfN1ogA3Y75raTOJQ2TwPQG95j yPWDx6yJYvh8dKRnpbF+uewMgDpHodUajLhwJmPnC6j5ChxHgb5mOq80tHqCgk11ybn2sIiD H6Z6k+tJNm1kfjieet8NlFlHlr999Z3FuQc2sMriZcc1GJbzpSZ8HwbkHviZNBS2Kbwdn0IF nYAx9/Y5hSg2VU2dynYgduoECXDhJc5NLzYKisM1ykw7t5HEvKR5b1Ax25up0ag6BjWar57l ysczv0n7DgbhfsIsUwj1Hb4YPhaEE9GMCjrjxnN4cq5qfAdfmG0arK9zkVWmMigSaqduUdbQ nmzKfJAVWdgq95yNl7Byii58Ib/Y9Pdd907swWV1gzflK5SMp17xZ9ozWJ3fGn6u3Mi0esyi xdjiIq7sIawIGJo5KulAxRcO269d4YJ9zrql6obgteO0tXlAMB6AjtSFsiNL7rgAHcIuP/gL QrLDDAstiLRB+/EBQHGoE40r3/VGtauL3DSJ30Cx5NnXBbbKEE64khcVWc4g5g+UAWyxYnid FxzoDUJ6Rj0p1NFmPpsKgX4FGLHpUKrbiw+Dp2HI1xa42Qgrw/cY8WG6eZ3GGdd5pzkrwiWI CqefwsOAWxBUx6GGkjiIrS0o9zY8q2bAvG0af7WbvOCpIk8H7+Bl4qoyYZn8zGKcMCXPzxhC +YxnE9bUjZ1FoyOkjELAUT7jgrraMiW7Fe58yxz9IWk9ejzHRjo7s2JAqdTNtNm/1a3h72CP qiennQxLzEQzZ4KyXLSrdpXlFcPlyFjcSWsGrUcpGbMSqzXgKpeEx8cbWt6KsJJ66s22gQFN 9Tcj5v50btxj/h9DFkgNxSpgsayeckDOH2wLnvFGUCMcrGeJHjIx9r9J6akRvtcgaQcthG9v yqaD162PjmHkGqMNVjnOuVNgSeHeR1G7djmI1A0WC6zEpS6Mk7eUpc/lzA9zLwqi2mfMGcdN WI5aEZRtviK6igehPxjGmtH534jLO+emi/f4fOLT/Re+fZtHClwkPpXpXogzL4ApjtDX+d/l THdhtt2ohS9jfLJzSBoGkkryH4DlMeQsENuNL+MvIFHQmrB9QkR4H+4CQkMoJ1gEtyquKRLw J7KjK21JDoIoLe2tYMMQsPTLsyAKn8oNxHkTSXVAAUyRjmuLWjDhkZZnZl6E1WQtpl/sYf33 p0URe0DPLTUPvEHDEMjGcQDZZRzRTlilKaUysIFtyLWRPb5Qd1b+4vYTbSVG/q9cV6k IronPort-Data: A9a23:W+6WtKwpy0s1RUA+Npp6t+fQwCrEfRIJ4+MujC+fZmUNrF6WrkVSn 2YeCjjTOfmCa2DwLY9xatzg8htT6JeEy4diTVM6/FhgHilAwSbnLYTAfx2oZ0t+DeWaERk5t 51GAjXkBJppJpMJjk71atANlVEliefQAOCU5NfsYkidfyc9IMsaoU8lyrVRbrJA24DjWVvd4 oqq+qUzBXf8s9JKGjJMg068gEg31BjCkGtwUosWOJinFHeH/5UkJMp3yZOZdxMUcaEIdgKOf Nsv+Znilo/vE7jBPfv++lrzWhVirrc/pmFigFIOM0SpqkAqSiDfTs/XOdJEAXq7hQllkPh26 dJxma2KQj4qGYGTm9QAYVpxPwhhaPguFL/veRBTsOSR0kvBNX70wrBtCFo8e4gA9aB7DAmi9 9RBc2FLN0HF17zwnOrTpupE3qzPKOHxO5gEsHx6whncFfdjWo/YBaLQ6re02R9t3p4QTKqGP 6L1bxJmPQbmYBNSHG41Cakfmd2UmmKhUQJh/Qf9Sa0fuTGIlVchgdABKuH9dMSNWdlUk1ywt GPD9X7wRBAcLt2WjzSfmlqnj+rL2Cf6Q546D6y97vcsgVuJx2VVBgd+aLegifukjEn4Xspeb k8Q4SBoqLA9skCmJjXgY/GmiHmluSIwauBbKu4dxF6O+rfmoC+1L3dRG1atd+canMMxQDUr0 HqAkNXoGSFjvdWppZS1qOz8QdSaZ3J9EIMSWcMXZVZcuYiy++nfmjqeEoc6SMZZm/WvQWmY/ tyckMQpr5k+5fPnOo254FbAxTe0p93KShU/oADPUSSp42uVhbJJhaT2uTA3Dt4Zce51q2VtW lBZwaByC8hTV/mweNSlGrllIV1Qz6/t3MfgqVBuBYI90D+m5mSue4tdiBknehkwYpZYI2SwO R6P0e+02HO1FCT0BUOQS93tY/nGMYC6SYSNug38MYseMscqKmdrAgkzPRDIhggBb3TAYYllY MzCKpb9ZZrrIahq0SatTOcQyvclwTolzmPOQ5/gyRm7w9KjiI29Ft843K+1Rrlhtsus+VyNm /4Gbpvi40gBDIXWP3eGmaZNdgpiBSZgWvjLRzl/K7TrzvxOQj9xUpc8ANoJJuRYokiivruRp S3mAxAGljISRxTvcG23V5yqU5u3Nb4XkJ7xFXVE0Y+A1ydxbICxwr0YcpdrL7Ar+PY6lKxxV /hAYNqbRPNVRW2fqTgaaJD8qq1kdQiq3FvUZXL8OmJgI5MwFRbU/tLEfxf08HVcBCSAs8Zj8 aar0RnWQMZeSgk7VJTWZfujwkmfp38YnO4uDULELsMKIRfp6IkvMDPqyPgtLJhUexnEwzKb0 SeQAAsZ/LCX+ddsqoOW2a3d9tWnCepzGEZeDlL317fuOHmI5HenzK9BTP2MIWLXWlTy9fjwf u5S1fz9bKAKkVsW4YpxF7FnkfA369f1/ecIzBliGzPOd1XuCbd7KD+DxcYJuqAUnu1Vvg6/W 0Su/NhGOOzVaZ2/TwNLfFIoPraZyPUZujjO9vBrck/00y9A4+TVW0tlPy6KhXEPN7ByKo4kn Lks4ZZE9wylhxM2Gd+alSQIpX+UJ3kNXvl1rJ0cG4O32AMnxksYOc7eFynxppSXapBPNlIgZ DqMi+zOiu0ElEbFdnMyE1nL3PZc3Mhf5koVkQVaf1nZyMDYgvIX3QFK9WplRApiziJYjbB5N F9rAEt4ePeV9DByickeAW31Q1NdBAeU81DawkcSkDGLVFGhU2HAIQXR4wpWEJz1J46dQtRaw F1c4GT4VzGsednwmyg2QkQjruTsC9B8nuEHdAZLAOzdd6TWoxK86kNtWYbMgx7/AIYqm1aBo vNllAq1QbOuLjYe+sXXFKHDvYn9i3m4yKhqROlgubgWBifbYj7aNf1i7ayuUpslGsEmOnNUx yCjygyjmvh+OOuzQugnOJMx IronPort-HdrOrdr: A9a23:Y/bfuK8jQ8bg5DYORaZuk+ASI+orL9Y04lQ7vn2ZhyYlEPBw9v rDoB1/73TJYVkqKRIdcLy7WZVoBEm9yXcK2/h1AV7SZmbbUQKTRekJgLcKgQeQfxEWndQy6U 4PSdkYNDSJNykdse/KpDKDKv4F7Z2t+LvAv5ak815dCTpRUolFwkNDBh+cCVAefng/ObMJUK Gn3+Jiin6bc3INYq2AdwA4Y9Q= X-IronPort-Anti-Spam-Filtered: true X-IronPort-AV: E=Sophos;i="5.93,277,1654552800"; d="scan'208,217";a="50669400" X-MGA-submission: =?us-ascii?q?MDENmNfChie8N6bWJ2Ds3dnjW2/zeU/PEnaqT0?= =?us-ascii?q?0cAycGC519AoxbLgfvK9R6A2eztva56QQAfg0UFC25OGrBYAdnlcdDO8?= =?us-ascii?q?p7X1cs4qmaPdKajMqdiHSu9pxMQi+aLNp+mmAGdeZ/lbYcKj9D2tf1aG?= =?us-ascii?q?+KZVXlnBTNs+xWYeMD324Vhg=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 11:42:05 +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=QDho4MjK1GxASMYAo8iV8euTOELtcqGegJkadkKd0nM=; b=JXL9JJA5yHE7HO0mE0GZ065rHd fM+RzXrMdI5Jgk2IFTYgzhKDbpnjHa3js1R9NteMo1UQkXBGA+tQToopLkxxzh1Tsg8FHB/X8SBw6 uOU+VA+1iukcaf0qOB4my5BMkaruR2tJlYJ85bVqX9c/F3sN5vRUVkO+6Xq7N2Q25cI8=; Received: from srv-00-62.mpi-klsb.mpg.de ([139.19.86.27]:55658 helo=max.mpi-klsb.mpg.de) by juno.mpi-klsb.mpg.de (envelope-from ) with esmtps (TLS1.3:ECDHE_RSA_AES_256_GCM_SHA384:256) (Exim 4.92) id 1oTKEP-00047f-Bj; Wed, 31 Aug 2022 11:42:04 +0200 Received: from [212.30.36.148] (port=61758 helo=smtpclient.apple) by max (envelope-from ) with esmtpsa (TLS1.2:ECDHE_SECP256R1__RSA_SHA256__AES_256_GCM:256) (Exim 4.94.2) id 1oTKEO-006sfP-Qc; Wed, 31 Aug 2022 11:41:56 +0200 Content-Type: multipart/alternative; boundary="Apple-Mail=_B4D1708F-1A5B-4BB7-8DD6-CFF427023B5A" 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 11:41:55 +0200 Cc: =?utf-8?Q?Fran=C3=A7ois_Pottier?= , caml-list@inria.fr Message-Id: <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> 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: 9C63A771-E4AD-42E4-A889-56CB1FFB563E@mpi-sws.org X-RSPAMD-Bar: / Subject: Re: [Caml-list] coinductive data types --Apple-Mail=_B4D1708F-1A5B-4BB7-8DD6-CFF427023B5A Content-Transfer-Encoding: quoted-printable Content-Type: text/plain; charset=utf-8 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 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). 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]. (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.8182) > 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 --Apple-Mail=_B4D1708F-1A5B-4BB7-8DD6-CFF427023B5A Content-Transfer-Encoding: quoted-printable Content-Type: text/html; charset=utf-8
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

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

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].

(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=_B4D1708F-1A5B-4BB7-8DD6-CFF427023B5A--