Re: [Caml-list] coinductive data types

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

On Tue, 30 Aug 2022 at 12:12, Xavier Leroy
<xavier.leroy@college-de-france.fr> wrote:
>
> On Tue, Aug 30, 2022 at 9:24 AM 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.

Hello Xavier,

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 ?

>> 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
>>
> Lazy evaluation (type Lazy.t) can also be used to define coinductive data structures.
>
> For concreteness, here are two definitions of the type of streams (infinite lists) :
>
> type 'a stream = unit -> 'a streamcell and 'a streamcell = { head: 'a; tail: 'a stream }
> type 'a stream = 'a streamcell Lazy.t and 'a streamcell = { head: 'a; tail: 'a stream }
>
> and of the stream of integers starting from n :
>
> let rec ints n = fun () -> { head = n; tail = ints (n + 1) }
> let rec ints n = lazy { head = n; tail = ints (n + 1) }

Thank you, yes I am familiar with this type of usage.

Regards,

Aaron

>>
>
> Hope this helps,
>
> - Xavier Leroy
>
>
>>
>> --
>> 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.