Hi Aaron, You might be interested in looking at CoCaml. It was developed by Jean-Baptiste Jeannin as part of his PhD, in collaboration with his advisor Dexter Kozen and Alexandra Silva. https://www.cs.cornell.edu/Projects/CoCaml/ Cheers, -N On Tue, Aug 30, 2022 at 8:38 AM Aaron Gray wrote: > 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 > 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. >