Hi Peter,
yes, I think they are different things. With (nominal) algebraic data types:
type peano = Z | S of peano
type nat = Z | S of nat
let f (x : peano) : nat = x -- type error
But with iso-recursive types:
type peano = mu peano. 1 + peano
type nat = mu nat. 1 + nat
let f (x : peano) : nat = x -- ok
Of course, it is merely a pragmatic choice that ML (and many other languages) treats algebraic types as nominal. It could just as well treat them as structural. In a sense, OCaml’s polymorphic variants behave more iso-recursively than its data types (at least until you activate --rectypes and opt into equi-recursive semantics).
FWIW, some old notes by Crary et al. [1] discuss this very choice, and how it interferes with modules. Moreover, based on their observations, the Harper/Stone semantics for SML actually models data type definitions as opaque abstract types (modules, really) that are merely _implemented_ by an iso-recursive type. That is both to capture their nominal (generative) semantics, but also to be able to express partial abstraction of mutually recursive types:
module type S =
sig
type t
type u = U of t
end
module M : S =
struct
type t = T of u
and u = U of t
end
This is not expressible directly with iso-recursion, as explained in [1].
(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
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/