Re: [Caml-list] coinductive data types

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

Hi Aaron,

No, there is no physical coercion involved.
Polymorphic variants have a uniform representation of constructor tags
(through a hashing function) so that (`Cons(1, lazy `Nil)) has always the same
representation, be it as int seqc or int aseqc.
So we are just talking about the different types the same value can be given.

Jacques

> 2022/08/31 12:22、Aaron Gray <aaronngray.lists@gmail.com>のメール:
> 
> Jacques,
> 
> I will get a raw OCaML Docker image, and have a play with this.
> 
> What is going on there, does ':>' return a conversion function as well
> as being 'true' and secondly a predicate ?
> 
> Thanks,
> 
> Aaron
> 
> 
> 
> On Wed, 31 Aug 2022 at 02:15, Jacques Garrigue
> <jacques.garrigue@gmail.com> wrote:
>> 
>> 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>のメール:
>> 
>> 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.
>> 
>> 
> 
> 
> -- 
> Aaron Gray
> 
> Independent Open Source Software Engineer, Computer Language
> Researcher, Information Theorist, and amateur computer scientist.