Hello François,

Thanks for putting me straight on that.

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.

I am looking on how to go about this and using coinduction and
bisimulation seemed like the best fit or correct way to go about this.

Does OCaML use/handle subtyping of mutually recursive algebraic data
types ? And if so, is its implementation easily accessible ?

Sorry I got you and Xavier muddled up somehow !

Regards,

Aaron

On Tue, 30 Aug 2022 at 08:24, François Pottier
<francois.pottier@inria.fr> wrote:
>
>
> Hello,
>
> Le 29/08/2022 à 17:43, Aaron Gray a écrit :
> > Does either ML or OCaML have coinductive data types ? And if so could
> > you please point me at the/some appropriate documentation on them.
>
> ML and OCaml have algebraic data types, which are recursive (that is,
> more general than inductive and co-inductive types). Algebraic data
> type definitions are not subject to a positivity restriction, and
> algebraic data types can be constructed and deconstructed by recursive
> functions, which are not subject to a termination check.
>
> If you want to see a typical example of a "co-inductive" data structure
> encoded in OCaml, I suggest to have a look at "sequences", which can be
> described as potentially infinite lists:
>
>    https://v2.ocaml.org/api/Seq.html
>
> --
> François Pottier
> francois.pottier@inria.fr
> http://cambium.inria.fr/~fpottier/



--
Aaron Gray

Independent Open Source Software Engineer, Computer Language
Researcher, Information Theorist, and amateur computer scientist.