Re: [Caml-list] coinductive data types

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

[-- Attachment #1: Type: text/plain, Size: 3501 bytes --]

Hello Aaron,

If you are interested in the subtyping already available inside OCaml,
it provides width subtyping for both objects and polymorphic variants.
Polymorphic variants are algebraic datatypes, but their equality is
structural rather than nominal, and they are limited to regular type
definitions.

For instance, the following subtyping on two variants of potentially infinite
streams is available:

type 'a seq = 'a seqc lazy_t and 'a seqc = [`Nil | `Cons of 'a * 'a seq]
type 'a aseq = 'a aseqc lazy_t
 and 'a aseqc = ['a seqc | `App of 'a aseq * 'a aseq]
let sub x = (x : 'a seq :> 'a aseq)
(* val sub : 'a seq -> 'a aseq *)

Jacques Garrigue

> 2022/08/30 21:33、Aaron Gray <aaronngray.lists@gmail.com <mailto:aaronngray.lists@gmail.com>>のメール:
> 
> On Tue, 30 Aug 2022 at 12:12, Xavier Leroy
> <xavier.leroy@college-de-france.fr <mailto:xavier.leroy@college-de-france.fr>> wrote:
>> 
>> On Tue, Aug 30, 2022 at 9:24 AM François Pottier <francois.pottier@inria.fr <mailto: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 <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 <mailto: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.


[-- Attachment #2: Type: text/html, Size: 24213 bytes --]