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
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 wasregarding how to go about implementing subtyping of mutually recursivealgebraic data types.I am looking on how to go about this and using coinduction andbisimulation seemed like the best fit or correct way to go about this.Does OCaML use/handle subtyping of mutually recursive algebraic datatypes ? 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 GrayIndependent Open Source Software Engineer, Computer LanguageResearcher, Information Theorist, and amateur computer scientist.