[Caml-list] Generating coinductive elements

[Jean-Baptiste Jeannin <jeannin@cs.cornell.edu>]

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