Re: [Caml-list] coinductive data types

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

Hi Andreas,

> On 31. Aug 2022, at 11:41, Andreas Rossberg <rossberg@mpi-sws.org> 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?
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 <cycle>
# let unfold (`Fold v) = v;;
val unfold : [< `Fold of 'a ] -> 'a = <fun>


> 
> 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!

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 <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/
>> 
>