Re: [Caml-list] coinductive data types

[Basile Clement <basile@clement.pm>]

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

Hi Andreas,

> (I’ve 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 – then a
> nominal semantics in the target language essentially breaks separate
> compilation/linking.)

This is interesting to me, do you have a pointer to these discussions
if they are public?

Best,
- Basile

> 
> Best,
> /Andreas
> 
> [1] Crary, Harper, Cheng, Petersen, Stone. Transparent and Opaque
> Interpretations of Datatypes, 1998
> (https://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.41.8182)
> 
> 
> > On 31. 8. 2022, at 10:46, Peter Thiemann
> > <thiemann@informatik.uni-freiburg.de> wrote:
> > 
> > Hi François 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çois Pottier
> > > <francois.pottier@inria.fr> wrote:
> > > 
> > > 
> > > Hi Andreas,
> > > 
> > > Le 30/08/2022 à 18:45, Andreas Rossberg a écrit :
> > > > 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.
> > > 
> > > 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çois Pottier
> > > francois.pottier@inria.fr
> > > http://cambium.inria.fr/~fpottier/
> > 
> 


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