Dear caml-list,
I have recently been interested in programming with coinductive
datatypes, like streams or infinite trees. I would like to create
functions that return coinductive elements, but I am having trouble
generating them on the fly, inside a function. Specifically, my function
typically creates a set of equations uniquely defining a coinductive
element, but I do not see any way of generating the corresponding
coinductive element. The equations I get always have just a variable on
the left-hand side, and an expression, possibly involving variables, on
the right-hand side. The relevant section of the manual is paragraph 7.3
(http://caml.inria.fr/pub/docs/manual-ocaml/manual021.html#toc70).
Let us take an example using streams (infinite lists) of numbers:
type stream = Cons of int * stream
let rec ones = Cons(1, ones) (* stream 1, 1, 1, 1, 1, 1, ... *)
let rec zero_ones = Cons(0, Cons(1, zero_ones)) (* stream 0, 1, 0, 1, 0,
1,... *)
Given the equations (**):
var0 = Cons(0, var1)
var1 = Cons(1, var0)
I would like the stream zero_ones to be generated.
Similarly, given the equation:
var1 = Cons(1, var1)
I would like the stream ones to be generated.
I have a few ideas, but none of them completely satisfying:
Idea 1 (works, but unsatisfying): print the equations with a "let rec "
in the front and the " and " word between equations. This prints some
code which, if executed, creates the desired coinductive element. It
runs fine, but it is very unsatisfying as I have to do a copy-paste in
an interpreter each time I call it, and to my knowledge there is no eval
(a la javascript) command in OCaml. The very reason why I cannot do the
let rec inside the function is that I would like it to work for any
number of equations.
Idea 2 (works, but unsatisfying): make the coinductive part of the type
a reference:
type stream = Cons of int * (stream ref)
Doing this, is is possible to build the desired element, but with
references and indirections all over. Because of the references, we can
look at equations one by one and build the coinductive element node by
node, creating loops when necessary. It runs fine as well, but using
references like this feels very unnatural, more like a hack, and not in
line with the OCaml philosophy. I also don't get the desired type at the
end, and I see no way to convert it to suppress the ref in the type.
Idea 3 (does not work): convert the list of equations to just one
equation on a list of streams, then call let rec. For example, in the
equations (**), we would write x = [var0; var1] and replace (**) by:
x = [ Cons(0, (List.nth x 1)); Cons(1, (List.nth x 0)) ]
Then take (List.nth 0 x) to get the result. This is more satisfying
because it does not involve changing the type or copying and pasting
some code at each execution, but it does not work. In a nutshell, OCaml
rejects this expression because is not allowed to call List.nth on the
recursive element x (see section 7.3 of the manual for more information):
# let rec x = [ Cons(0, (List.nth x 1)); Cons(1, (List.nth x 0)) ];;
Error: This kind of expression is not allowed as right-hand side of `let
rec'
To me, both ideas 1 and 2 are unsatisfying, and idea 3 simply does not
work. It would be extremely useful if anyone knew how I could do this,
or, if it is not possible, show me why it is not.
Thank you,
Jean-Baptiste Jeannin
--
Caml-list mailing list. Subscription management and archives:
https://sympa-roc.inria.fr/wws/info/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs
