Re: [Caml-list] coinductive data types

["François Pottier" <francois.pottier@inria.fr>]

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/