Re: [Caml-list] coinductive data types

[Peter Thiemann <thiemann@informatik.uni-freiburg.de>]

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/