Re: [Caml-list] coinductive data types

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

Hi François,

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. That matters in so far as it makes them modular in a way that true nominal types are not.

Iso-recursive types would only behave like nominal in the degenerate case where all type definitions occurring in the entire program (across module boundaries) are tied into a single grand iso-recursive knot, I think.

/Andreas


> On 30. 8. 2022, at 17:47, François Pottier <Francois.Pottier@inria.fr> wrote:
> 
> 
> Hi,
> 
> On 30/08/2022 14:37, Aaron Gray wrote:
> > My original path of inquiry which I should have actually stated was
> > regarding how to go about implementing subtyping of mutually recursive
> > algebraic data types.
> 
> Do you mean implementing an algorithm that decides whether two types are
> related by subtyping, in the presence of mutually recursive algebraic
> data types?
> 
> I guess the answer depends on exactly how the subtying relation is defined.
> E.g., if "α foo" and "β bar" are (parameterized) algebraic data types, does
> the subtyping relation "α foo ≤ β bar" necessarily imply that "foo" and "bar"
> are the same algebraic data type?
> 
> - If the answer is positive, then the problem boils down to deciding
>  "α ≤ β" or "β ≤ α" or neither or both, depending on whether this
>  algebraic data type is covariant or contravariant or neither or both.
>  In that case, you are working with "isorecursive" types,
>  also known as "nominal" types.
> 
> - If the answer is negative, then (I imagine) you wish to unfold the
>  definitions of "foo" and "bar" and decide whether the two unfoldings
>  are related by subtyping.
>  In that case, you are working with "equirecursive" types,
>  also known as "structural" types.
> 
> Brandt and Henglein ("Coinductive axiomatization of recursive type equality
> and subtyping", 1998) study the second problem, if I remember correctly.
> 
> > Does OCaML use/handle subtyping of mutually recursive algebraic data
> > types ? And if so, is its implementation easily accessible ?
> 
> OCaml has explicit subtyping coercions: a user can write `(e : t1 :> t2)`
> and the compiler will check that `t1` is a subtype of `t2`.
> 
> As far as algebraic data types are concerned, OCaml's notion of subtyping is
> nominal, I believe. An algebraic data type can be decorated with variance
> annotations, so, for instance, "list" can be declared covariant and "α list"
> is considered a subtype of "β list" if α is a subtype of β. However, "α list"
> can never be considered a subtype of an algebraic data type other than "list".
> 
> The variance annotations provided by the programmer are checked when an
> algebraic data type is defined, and are later used when deciding whether a
> subtyping relation holds.
> 
> Some more information here:
> 
>  https://blog.janestreet.com/a-and-a/
>  https://v2.ocaml.org/manual/expr.html#ss%3Aexpr-coercions
> 
> --
> François Pottier
> Francois.Pottier@inria.fr
> http://cambium.inria.fr/~fpottier/