From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q3UGaPLf025223 for ; Mon, 30 Apr 2012 18:36:25 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AnABAA6/nk+AVGeLe2dsb2JhbABEr0iDIgEBFiYFIoILPUA9FhgDAgECAUsNCAEBiAkLmHWYFokJkSIEiDCOX4RljVA X-IronPort-AV: E=Sophos;i="4.75,505,1330902000"; d="scan'208";a="156183050" Received: from mail-hub-2.cs.cornell.edu (HELO exch-hub2.cs.cornell.edu) ([128.84.103.139]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-MD5; 30 Apr 2012 18:36:16 +0200 Received: from [128.84.98.107] (128.84.98.107) by mail.cs.cornell.edu (128.84.103.140) with Microsoft SMTP Server (TLS) id 8.3.245.1; Mon, 30 Apr 2012 12:36:14 -0400 Message-ID: <4F9EBF8C.2060309@cs.cornell.edu> Date: Mon, 30 Apr 2012 12:36:28 -0400 From: Jean-Baptiste Jeannin User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:10.0.2) Gecko/20120216 Thunderbird/10.0.2 MIME-Version: 1.0 To: Content-Type: text/plain; charset="ISO-8859-1"; format=flowed Content-Transfer-Encoding: 7bit Subject: [Caml-list] Generating coinductive elements 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