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

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/