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
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 }