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 41596E0133 for ; Tue, 30 Aug 2022 20:20:33 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jnfoster@cs.cornell.edu; spf=Pass smtp.mailfrom=jnf27@cornell.edu; spf=None smtp.helo=postmaster@mail-io1-f47.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of jnfoster@cs.cornell.edu) identity=pra; client-ip=209.85.166.47; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="jnf27@cornell.edu"; x-sender="jnfoster@cs.cornell.edu"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of jnf27@cornell.edu designates 209.85.166.47 as permitted sender) identity=mailfrom; client-ip=209.85.166.47; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="jnf27@cornell.edu"; x-sender="jnf27@cornell.edu"; x-conformance=sidf_compatible; x-record-type="v=spf1"; x-record-text="v=spf1 ip4:35.190.247.0/24 ip4:64.233.160.0/19 ip4:66.102.0.0/20 ip4:66.249.80.0/20 ip4:72.14.192.0/18 ip4:74.125.0.0/16 ip4:108.177.8.0/21 ip4:173.194.0.0/16 ip4:209.85.128.0/17 ip4:216.58.192.0/19 ip4:216.239.32.0/19 ~all" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-io1-f47.google.com) identity=helo; client-ip=209.85.166.47; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="jnf27@cornell.edu"; x-sender="postmaster@mail-io1-f47.google.com"; x-conformance=sidf_compatible IronPort-SDR: 36kaMtTbDCavRAh82/dHUo1c8R0cmXRPtSXHe4A6AkqLvmohgZTk+Tl6hF+3GpNmkRSQJetYoQ EpNQFt9Q8cDnl5AU19NHhA0HRnSJ/dQE/fIhX4aG6QcOZtj/fAggu+ikJ7YgVU2NEa6GzcVdZT zv6gWBx2r6w6rZLn66/SO6qcgGb1ngY1e79imkZExs7PVZXdGCFAQSPWlhcoNUhqpe2TdiTEqG o5WKBIE6zbeL9U3637wPmxseoV2n9yy0jSMPehw4G3IlKT8SNjvGzEWPNy6f19+MEJVn7+wQ2r Eb4GSkBfhRe9brgU92UYTcsF X-IPAS-Result: =?us-ascii?q?A0A+AgApVA5jfy+mVdFaHAEBAQEBAQcBARIBAQQEAQGCD?= =?us-ascii?q?4IkgVcvBAtFhE6BI49tiySLGohDCQEDAQ0sARUEAQGJbQIdBwEENBMBAgQBA?= =?us-ascii?q?QEBAwIDAQEBAQEBAwEBBQEBAQIBAQIEBAETAQEYCRkHDg4FPmRogU+BdAtBg?= =?us-ascii?q?jUpAYNjAQEBAQIBARERVgULCwQHDSoCAiEBBgwBBQEcBhMigluCbgMNJQOcH?= =?us-ascii?q?IEEQoo4eoExgQGHKQ1RCYFyEoErhnuBQQEBh1YnHIINgUuCdD6CIIV6gmUEh?= =?us-ascii?q?BaTBwMEBQEGNwECAUQeQgMLQy8GHAMUAwUYDAcDGQ8jDQ0EFgcMAwMFJQMCA?= =?us-ascii?q?hsHAgIDAgYVBQICTTkIBAgEKyQPBQIHLwUELwIeBAUGEQgCCA4CBgQEBAQVA?= =?us-ascii?q?hAIAgcBJggPBxMzGQEFCk8QCSEcDhoNBQYTAwsVbQVFDygzNTkrFQgbCj1VK?= =?us-ascii?q?igVAwQEAwIGEwMDIAIQLDEDFAYpExItByt1CQIDImgFAwMEKCwDCT4HKCY8B?= =?us-ascii?q?QVZOgEEAwMQIj0GAwkDAidfZAGYM4MSwXFug1yYLoF0hgQyqHYdlmqRHJY0E?= =?us-ascii?q?COBVSOBWzMaCB0TOzEGgjBOAQIBAg0BAgIDAQIBAgkBAQKdCSgxOwIGAQoBA?= =?us-ascii?q?QMJilIBAQ?= IronPort-PHdr: A9a23:cflYpBzB8y85Z3HXCzLLwFBlVkEcU1XcAAcZ59Idhq5Udez7ptK+Z heZv6U2xwaTBs3y0LFts6LuqafuWGgNs96qkUspV9hybSIDktgchAc6AcSIWgXRJf/uaDEmT owZDAc2t360PlJIF8ngelbcvmO97SIIGhX4KAF5Ovn5FpTdgsip2e2+4YPfbgZGiTayfL9+M hu7phjNu8cLhodvNrw/wQbTrHtSfORWy2JoJVaNkBv5+8y94p1t/TlOtvw478JPXrn0cKo+T bxDETQpKHs169HxtRnCVgSA+H0RWXgLnxVSAgjF6Bb6Xortsib/q+Fw1jWWMdHwQLspQjmp8 btlRwH0hycGLz458X/YispsjKJAvRmtowVzz5PIbI2JMfZzeL7Wc9EHSmpbRsteWCJBDYG8Y YUBDOQPIPhWopfhqFYVtxSyGROhCfnzxjNUhHL727Ax3eQ7EQHB2QwtB8oAv27IrNrrKawcU ee1zLLUzTrddfNdxDDw6IrOchAvpvGMRq5wftTLyUQ0CwzFlU+cppDiPzOP0OQCrWyb7+56W e2xlmEnthh8rz6yzcgjlofHnJgaykzY9Spn2oY1I8W1RUp0b9K5DpdeuSGXOoVrT888X21mt yk0x78HtJKnYiUHzIgqyhHdZvKIbYSF/hbuWemfLDp7mH9pZr2yigu8/0Wm1+byVdG03U5Uo iZZltTArHMA2hzJ5sSaS/Zw/12t1DmN2g3V9+pKO1o7lbDBJJ4k2rMwloQcsUDEHiLunUX5l q6WdkE99uip7OTrf6zqppGTOoJ2kA3+PaMumsuwAeQ8LAcCRXSU+eO51LH7/E35RqtFjuEun 6XHrJzXId4Xq625DgNPz4ou6heyAy2p3dkahXUHKUhKeBODj4jnIVHOJ/X4AO+9g1Sqnjdn2 fLLM6b9DZXKNHjDlqnufbJ560JG1gU80M1f64pSCr4aOP3zQFP+tMTEDh8lNAy52/vrBM1n1 owCQWKPHrOZMKTKvFCU/O0vJu2MaJYRuDb8MPgl++XjjWQ5mF8YZammx4EbaHG+HvR8IkWWe 2DggtkbETRCgg1rZeXwj1vKfiRadj7mVqsm4Tc9B5ivHMHHR5uxm5SO2S66GttdYWUQWX6WF nK9UYyYVr8ibzmOL9Upxj4CW7+6V4I7/Rq18gT90bxqKu6S9yEF48GwnONp7vHewElhvQd/C N6QhiTUFzkcdgIgQjY32Po6uklh0hKZ1qM+hfVEFNtV7vcPUwEgNJeawfYpQ8vqVFfnedGEA E2jXs3gGSs4G9A3zdgVf0tnM965yBvExSynB7tTmrCWV9Qv6qyJ53HqPI5mzmrekqwojl0oW MxKYG+giPQg3wPUHYjEl0Hfmqq3JuwHxCCY0mCFwCKVuV1AFg59VaKQRXcEek7ftsj0/GvHR r6qTLUga05PlZHEJaxNZdnky15BQZ8PIfz4ZGS80ye1DBeMnPaXaZbyPn8a12PbAVQFlAYa+ TCHMxI/D2GvuTCWCjsmDl/pb072lIs24HqmUk85yR2LZEx9xvK0/BASn/mVV/IU2PoNpi4gr zx+GFv10cjRDpKMoA9ofaMUZt1Ygh8P12TXsBdhM4aIJLskjVkEdQlzuwXj2wg2QoRMnM42r W87mRJoIPH9shsJfDeZ0Jbsf7zPfzOqrVb/NuiPhA+YjInFn8VHoO41oFjiogyzQ08r8nE9l sJQz2PZ/JLBSgwbTZP2VE8zsRl8vbDTJCcntOa2nTVhN7e5tjja1pcnHuwgn1yiedkFb4uPE xX0HskeQcWiNaZ5/jrhJgJBJ+1U+KMuaomkcfWBw7KmJs5rh3Stin5B7YR5lE+A6mAvL4yAl 4ZAyPae0AydUj76h1r0qcH7l7dPYjQKF3a+wyzpbGJITpV7Zp1DSWKnIsntg857m4aoQXlTs liqG1IB3satPxuUdV30mwNKhwwbpnmumC3wyDIR8XlhrKyRhnPmyOP4chcDPihGSHQqgVr3I IeyhswXRwDyN1lvxEbjvBikgfQE7K1kZ3HeW0JJYzT7IwQAGuOru7yObtQOoJIkvCNLUfitN FWTS7rzuRwfgGvoG2pTwix+din/4M2o2UwnzjvDcjAv8ym8G4k43xrU6d3CSOQE2zMHQHM9k jzLHh2mONLv+9yIlpDFu+T4VmS7V5QVfzO4qOHI/Ca9+2BuBgWy2v6pndiyWwo833Wk/9JtT yPFqBK6b4X2nfffU6ovbgxzCVnw5tAvUIN4nNFvrJoXw34XgpHT8HYa2zS7IZBQ3qTwa2AIT DgAzovO4QTr70ZkK2qA24PzUnjOp6kpL8n/eG4d3TgxqtxbEKrBpqIRhjN7+xDr5RKUe/V2m S0RjOcj+GJPyf9coxIjl0D/SvgTBRUKZnGqzkXQqYri8+MPIzzzObmoiBggwZb7V+rE+18EH i6+I8ZqHDcsvJshdguUijurrNmjIoG1D5pbtwXIwUmeybIJedRhzrxSwnA/cWPl4S96kahi0 Vo3jMv85M/eey1s5P7rXUIeb2eoIZtVona008M81o6Xx9z9R80xXGxUA924C6rvSmtatOy7Z V/RS3tl+yvdQfyHWlbBoEZ+8yCVS8HtZyzRfSNJi40lHUb4RgQXgRhIDm9jwNhkRkbzlZanK AAgt3gQ/gKq8EISjLgzZl+kCCGH4175IiE9TJzVRPZPxidF4UqdccmX7+YpWjpd4oXktguGb GqSewVPC2gNHE2CHVHqeLe0t5HG9KCDC+yyIuGrA/3GoPFCV/qO2ZOk05d3tzeKOMKVO3B+D vo9kkNdVHF9Es7dln0BUSsS3y7Kaseaol+79EgV5oin9+/3XQv0+YaVI75bMNEq+hfvxKnfa KifgyF2LTse3ZQJhDfJxLUZwF8OmnRuej2qQtFi/WbGSKPdnLMSDgZOMXsicpsVqftigE8RZ p2+6Ju9zLNzg/8rBk0QUFXgnpvsfskWOySnM1iBAk+XNbOALDmNwsftYKr6R6cD6Ycc/xC2p zufFFfuezqZkDy8HRKpP7sTpCqcJhpTvIX7fxpwQzuGLpqueligPdl7gCdji6UznW/PPHUAP CJUdkpMqviR6nodjKkgXWNG6XVhIK+PnCPTvIy6Yt4G9PBsBCpzjedT5n83nqBU4C9zT/twg CLOr9RqrjlOd8GE0XxsVwBIpzJPwo+HoBc6UU023pJHQ3DJ+BZL4GmNWU1iTzpND9Tuv+VRz YGKmv6sbjhF9N3Q8I0XAM2GcKq6 IronPort-Data: A9a23:neZrl607FWIMdE/ZZvbD5d93kn2cJEfYwER7XKvMYLTBsI5bpzQPm DNOWm6AO/jbZ2X3Ktp2at608EgO75WEndBjQQU93Hw8FHgiRejtVY3IdB+oV8+xBpSeFxw/t 512hv3odp1coqr0/0/1WlTZhSAgk/nOHNIQMcacUsxLbVYMpBwJ1FQywIbVvqYy2YLjW1PW4 YuoyyHiEAbNNwBcYjp8B52r80sHUMTa4Fv0aXRjDRzjlAa2e0g9VPrzF4npR5fLatU88tqBe gr25OrRElU1UPsaIojNfr7TKiXmS1NJVOSEoiI+t6OK2nCuqsGuu0o2HKJ0VKtZt9mGt85I0 PocvJiVdR40YPftmc05CEZIKggraMWq+JefSZS+mcmazkmDcny1hvsyUwc5OooX/usxCmZLn RAaAGpVP1bT2qTvnuz9FrYEascLdKEHOKsdvH86khnSCuwgTJTHBajG+Le02R9t3p0eRqmBN 6L1bxI/VEzCZg9SMGw8I888l8S6oyKnTjdX/Qf9Sa0fujCPlmSdyoPFO9PQfpmORN5Jtl2Jo 3rPuWX/GBATctKFoQdp6Vqpj+7L2CL8AcccSOL++fltj1megGcUDXX6SGdXv9Gns1aRCttbD nAN53R0jKkb0Bf0XuDUCkjQTGG/gjYQXN9ZEusf4Q6Ly7bJ7wvxOoTiZm4RADDBnJ9mLQHGx mNljPuyWmMy6Oz9pWa1s+bL/WnraED5OEdbPXdcJTbp9eUPt23as/4iZtNqEarwj9qsXD+sn HaFqy8xg7hVhskOv0lawbwlq2L9znQqZlRujukyYo5Dxl0hDGJCT9LwgWU3Fd4acO6koqCp5 RDoYfS24uEUFo2qnyeQWugLF7zBz6/bbmSD0AE+RMF6qG7FF5ufkWZ4sGEWyKBBYpZsRNMVS BK7Vf55v8INYiP7PcebnaroUpVynMAM6ugJptiNNoYUCnSAXACA+y5qaCatM5PFwSARfVUEE c7DK66EVC5EYYw+lWbeb7pDjNcDm39mrUuNH8yT50r8itK2OiXFIYrpxXPUMYjVGovf8FuLm zueXuPWoyhivBrWO3SKqddMcAFXfRDWx/ne8qRqSwJKGSI+cElJNhMb6elJl1VNk/sHm+HW0 Gu6X0MEmlPziWeecFeBbWplZbfrG5tzsCtjbyArOF+p3VklYJqusPZHLcBsI+F/+bwx1+NwQ tkEZ96EXqZFRAPB9mlPdpL6toFjKEmmiFvWbSqoaTQyZbB6QAnN9oO2dwfj7nBSXCGs88A5u but0gedTJYeHlwwAMHTYfOp7lWwoXlBybooBBCWeoFeIRy+/pJrJir9iu4MD/sNcRiTlCGH0 wu2AAsDobWfqYEC9tSU17uPqJ2kErcjE0dXQzvb4LKxOXWI92av29UbAuOBfDSYVWStvav+O qNayPbzNPBBl1FP6tIuH7FuxKM4xt3uu74KkVg+TSuTNwymWuF6P32L/chTrakRlLVXjg27B xCU8d5ANLTVZc7oTAwLKAw+YrjR3P0YgGOJv/E8IUG/5SguubTbDgNdOB6DjCEbJ7xwadt3z eAksc8Qygq+lht6bYrc334MrzyBfi4aTqEqlpAGG4u32AAl/VdPPM7HASjs7ZDTNthBPyHG+ NNPaHYuWlid+qbDT5b3PX3E3O4YhJNX/R4WkxkNIFOGnteDjfgytPGUHfLbUSwNpiirEcoqU oSoC6GxDa6J5TFlgMwFUmyxc+2ELAPM4VT/kjPli0WAJ3RFlQXxwKkVMv3L90cD9W9Yen5W8 KzwJKMJl9r1VJmZ4xbeknKJZxAuoRKdO+ECdA2a8xy5IqQH IronPort-HdrOrdr: A9a23:RKNUGKOKhYZnCcBcTvijsMiBIKoaSvp037Dk7TEWdfU1SL3gqy nApoV46faZskdzZJhko7C90cq7L080l6QFhLX5VI3KNGLbUSmTTb2KhrGSpwEIdReOkdK1Fp 0MT0G9MrfN5JRB4foSKTPWL+od X-IronPort-Anti-Spam-Filtered: true X-IronPort-AV: E=Sophos;i="5.93,275,1654552800"; d="scan'208,217";a="50583778" X-MGA-submission: =?us-ascii?q?MDFo/6jiNLYs4DlQwTZGB552ZjQ2l1hS04hOrB?= =?us-ascii?q?Hf5AR3u9Xy4M6q1dv40UzHay0+/1OPdG3bUpc11uBqOqx3FJz/bhf/Ry?= =?us-ascii?q?SpyKfBjkiAHJK3u9K7cndRZXsjzKzL2SoX3qcNcuDJ7hnUV+XwHccehF?= =?us-ascii?q?OArd9etQOKQawX7oakp5MXLA=3D=3D?= Received: from mail-io1-f47.google.com ([209.85.166.47]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/ECDHE-RSA-AES256-GCM-SHA384; 30 Aug 2022 20:20:31 +0200 Received: by mail-io1-f47.google.com with SMTP id p187so9950129iod.8 for ; Tue, 30 Aug 2022 11:20:31 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20210112; h=cc:to:subject:message-id:date:from:in-reply-to:references :mime-version:x-gm-message-state:from:to:cc; bh=E2OeSr1UhO9BsNfUipnO4Ej+Lzf61kzZmlQIrYI7jc4=; b=Et/ph2T9fnqbKMZCUyYWRA0KWcUZUmth+4vN1SBjmgUNX7gBRgrJzaJ2gC0itG8hfn MVUUe+4JOTB/qAlSt9msfkY/J9P6Fwic+56RQn3zKg0tGlzPxr6ylQxCGeWTAsAiRFQM vyvdypY4bgnPTGM4BSRX7x7rrlIKjiCcGO1MbNLzQ2VSp+TNV2gQ6LzWvMo2xQHLzkHC /b8ADAZ+0lFn+EYvbK4RBeIUlxfadkPPDM6LIvRMOh3oHUkpwxzPPgS2fKSzcdNEXtgn Dcz8YylNW2cf8tkMKPdbHjgmdDUBrzDJeW914Xi5UPk5y4K/EMxopp93jw349SAUQpNn djOA== X-Gm-Message-State: ACgBeo37VTyH3flmNa1A8nlQz4FyVAmAb/Lx19L3oiVgVG5yvxzC21us xmn8/6waOeXF1luqLdW6FybI0SwIAUssNJi9jxQPsQ== X-Google-Smtp-Source: AA6agR4ypbZX0gMATPicWviYTa5sG3Mr01T2DZ/Ae1dlb1NieeJ7KkphOOhZDSYVq2QWacdk51ujz8aV+NauaKfAGYc= X-Received: by 2002:a05:6638:13c6:b0:346:dad1:8b28 with SMTP id i6-20020a05663813c600b00346dad18b28mr13177951jaj.318.1661883630464; Tue, 30 Aug 2022 11:20:30 -0700 (PDT) MIME-Version: 1.0 References: <25e68e2c-04d2-7764-e189-00812c08a34a@inria.fr> <8078ad33-f220-b233-4863-06ce30cc8cff@inria.fr> <2C890C66-F8F7-402C-B88E-587C3E21DE89@mpi-sws.org> In-Reply-To: From: Nate Foster Date: Tue, 30 Aug 2022 14:20:19 -0400 Message-ID: To: Aaron Gray Cc: Andreas Rossberg , =?UTF-8?Q?Fran=C3=A7ois_Pottier?= , OCaML Mailing List Content-Type: multipart/alternative; boundary="00000000000073c74c05e7796f65" Subject: Re: [Caml-list] coinductive data types --00000000000073c74c05e7796f65 Content-Type: text/plain; charset="UTF-8" Content-Transfer-Encoding: quoted-printable For a clear, textbook treatment of these topics at the introductory (i.e., advanced undergrad or beginning graduate) level, it's hard to beat Benjamin Pierce's "Types and Programming Languages" (MIT Press, 2002). Chapters 20 and 21 cover the basics of recursive types including iso/equi-recursive types and subtyping. And the "Notes" section at the end has lots of references to a bunch of "founding papers" -- at least, as of 20 years ago. -N On Tue, Aug 30, 2022 at 1:01 PM Aaron Gray wrote: > On Tue, 30 Aug 2022 at 17:46, Andreas Rossberg > wrote: > > > > Hi Fran=C3=A7ois, > >> I=E2=80=99m curious why you would categorise iso-recursive types as no= minal. I > have always considered them structural as well, since two structurally > matching iso-recursive type expressions are still deemed equivalent. That > matters in so far as it makes them modular in a way that true nominal typ= es > are not. > > > > Iso-recursive types would only behave like nominal in the degenerate > case where all type definitions occurring in the entire program (across > module boundaries) are tied into a single grand iso-recursive knot, I thi= nk. > > Are there any founding papers or books on isorecursive and > equirecursive typing ? > > Aaron > --00000000000073c74c05e7796f65 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
For a clear, textbook treatment of these topics at th= e introductory (i.e., advanced undergrad or beginning graduate) level, it&#= 39;s hard to beat Benjamin Pierce's "Types and Programming Languag= es" (MIT Press, 2002). Chapters 20 and 21 cover the basics of recursiv= e types including iso/equi-recursive types and subtyping. And the=C2=A0&quo= t;Notes" section at the end has lots of=C2=A0references to a bunch=C2= =A0of "founding papers" -- at least, as of 20 years ago.

-N

On Tue, Aug 30, 2022 at 1:01 PM Aaron Gray &l= t;aaronngra= y.lists@gmail.com> wrote:
On Tue, 30 Aug 2022 at 17:46, Andreas Rossberg <rossberg@mpi-sws.org= > wrote:
>
> Hi Fran=C3=A7ois,
>> I=E2=80=99m curious why you would categorise iso-recursive types a= s nominal. I have always considered them structural as well, since two stru= cturally matching iso-recursive type expressions are still deemed equivalen= t. That matters in so far as it makes them modular in a way that true nomin= al types are not.
>
> Iso-recursive types would only behave like nominal in the degenerate c= ase where all type definitions occurring in the entire program (across modu= le boundaries) are tied into a single grand iso-recursive knot, I think.
Are there any founding papers or books on isorecursive and
equirecursive typing ?

Aaron
--00000000000073c74c05e7796f65--