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 q3UGpJIh025541
	for <caml-list@sympa-roc.inria.fr>; Mon, 30 Apr 2012 18:51:19 +0200
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: An0CANHCnk/UGyoClGdsb2JhbABEgx2sMoMAIgEBAQEJCwkJFAMkggkBAQQBUyUBBQsLIRYPCQMCAQIBRRMBBwEBiAQJuhqNfYMlBJV+hXaNNg
X-IronPort-AV: E=Sophos;i="4.75,505,1330902000"; 
   d="scan'208";a="156184150"
Received: from smtp2-g21.free.fr ([212.27.42.2])
  by mail1-smtp-roc.national.inria.fr with ESMTP; 30 Apr 2012 18:51:10 +0200
Received: from [192.168.1.3] (unknown [82.237.71.191])
	by smtp2-g21.free.fr (Postfix) with ESMTP id 158354B016C;
	Mon, 30 Apr 2012 18:51:05 +0200 (CEST)
Message-ID: <4F9EC2CF.5090202@inria.fr>
Date: Mon, 30 Apr 2012 18:50:23 +0200
From: Xavier Leroy <Xavier.Leroy@inria.fr>
User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:11.0) Gecko/20120412 Thunderbird/11.0.1
MIME-Version: 1.0
To: caml-list@inria.fr
CC: jeannin@cs.cornell.edu
References: <4F9EBF8C.2060309@cs.cornell.edu>
In-Reply-To: <4F9EBF8C.2060309@cs.cornell.edu>
X-Enigmail-Version: 1.4
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
Subject: Re: [Caml-list] Generating coinductive elements

Hello Jean-Baptiste,

> Let us take an example using streams (infinite lists) of numbers:
> 
> type stream = Cons of int * stream

You won't go far with this type for integer streams, as the only way
to construct values of this type is "let rec", and it's severely
restricted (because of call-by-value requirements).  For instance, you
can't even define the stream of all integers 0.1.2.3.4...

The proper OCaml type for integer streams is

type stream = Cons of int * stream Lazy.t

and with this type you should be able to do pretty much everything you
want to do with your equations.

HTH,

- Xavier Leroy