Re: [Caml-list] coinductive data types

[Andreas Rossberg <rossberg@mpi-sws.org>]

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

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

[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: 5752 bytes --]