> On 31. 8. 2022, at 17:40, Peter Thiemann wrote: > > Hi Andreas, > >> On 31. Aug 2022, at 11:41, Andreas Rossberg wrote: >> >> 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 > > Sure! > >> >> 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). > > With "pragmatic" you mean that type checking gets more efficient or do you have some other pragmatic aspects in mind? It probably also is easier to explain to many programmers and produces more readable error messages. > IIRC, polymorphic variants are just (open) sum types, which admit equi-recursion. Viz the behavior of the degenerate, one-armed polymorphic variant to "implement" iso-recursion: > > # let rec m = `Fold m;; > val m : [> `Fold of 'a ] as 'a = `Fold > # let unfold (`Fold v) = v;; > val unfold : [< `Fold of 'a ] -> 'a = Yes, I think you are right that equi-recursion is still observable, but this may be the wrong example. I think it merely shows that OCaml’s let-rec is a more general fixpoint, but that also works with ordinary data types: type t = Fold of t let rec m = Fold m let unfold (Fold v) = v But the following example should reveal the underlying equi-recursive semantics: # let f (x : [`Foo of [`Foo of 'a]] as ‘a) : [`Foo of 'b] as 'b = x;; val f : ([ `Foo of 'a ] as 'a) -> 'a = So yeah, strike my remark about polymorphic variants. :) > > >> >> 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]. > > Thanks for the pointer to this gem! Just to clarify and expand on my earlier remark, the way the Harper/Stone semantics eventually solved both problems was not by adopting “Shao’s equation” as predicted in those notes (which would require coinductive type equivalence, throwing a major advantage of iso-recursion out the window). Instead, they model the definition type t = A | B of t as (the equivalent of) open ( struct type t = mu t. 1 + t let A = fold (inl ()) let B x = fold (inr x) let case_t x f g = match x with inl y -> f y | inr z -> g z end : sig type t val A : t val B : t -> t val case_t : t -> (unit -> 'a) -> (t -> 'a) -> ‘a end ) This explains datatypes as a combination of iso-recursion and the existing semantics for type abstraction (which could in turn be explained as existential quantification, of course :) ). Cheers, /Andreas > > Best > -Peter > > >> >> (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 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 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/