Re: [Caml-list] coinductive data types

[Nate Foster <jnfoster@cs.cornell.edu>]

[-- Attachment #1: Type: text/plain, Size: 1307 bytes --]

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 <aaronngray.lists@gmail.com>
wrote:

> On Tue, 30 Aug 2022 at 17:46, Andreas Rossberg <rossberg@mpi-sws.org>
> wrote:
> >
> > Hi François,
> >> I’m 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. That
> matters in so far as it makes them modular in a way that true nominal types
> 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 think.
>
> Are there any founding papers or books on isorecursive and
> equirecursive typing ?
>
> Aaron
>

[-- Attachment #2: Type: text/html, Size: 1758 bytes --]