Re: [Caml-list] coinductive data types

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

On Tue, 30 Aug 2022 at 14:58, Nate Foster <jnfoster@cs.cornell.edu> wrote:
>
> 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/

Hi Nate,

Great, thanks, I have a lot to look at in this area, a bit of a
digression, but am looking at coinductive implementations, so thanks,
hopefully I will get round to checking it out.

Aaron

> On Tue, Aug 30, 2022 at 8:38 AM Aaron Gray <aaronngray.lists@gmail.com> 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
>> <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.



-- 
Aaron Gray

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