Re: [Caml-list] coinductive data types

[Aaron Gray <aaronngray.lists@gmail.com>]

Hi François,

On Tue, 30 Aug 2022 at 16:47, François Pottier
<francois.pottier@inria.fr> wrote:
> 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?

Yes exactly, as well as equivalence obviously..

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

I am looking at how to support both nominal and structural types in a language.
Basically at the top level with keywords 'transparent' and 'opaque',
both for type declarations,
and only narrowing 'opaque' for variable declarations and, as only
narrowing casts on value or type parameterization.

> Brandt and Henglein ("Coinductive axiomatization of recursive type equality
> and subtyping", 1998) study the second problem, if I remember correctly.

Yes I found this paper pretty early on and seems to be the founding
paper in this area, having said that, it does not seem to deal with
union and intersection types.

What I have gathered is that in order to have completeness of type
system and soundness you need the type system to be implemented as a
type lattice, there by underpinning the system on to a topological
space and thus being constructable and well founded.

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

Yes this is nice, covariance and contravariance annotations.

I don't know how accessible OCaML's, type system code is. I have had a
brief look, I am used to Haskell, and Haskell's type annotations in
order to get my bearings.

Are there any papers on OCaML's type system proper at all please ?

Many thanks for the comprehensive reply.

Aaron