The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

roconnor AT theorem.ca
 wrote:
> If I evaluate the expression let e:=stream in foo e e, with strict 
> evaluation under the virutal machine, and where stream is some 
> infinite co-inductive stream, will the computation for stream be 
> shared, or will stream just be copied twice into foo, an each copy 
> will be evaluated independently?
>
> Thanks.
In my experience, co-inductive data-types have good laziness properties.
Here is a small example that you could run to convince yourself:

CoInductive Stream : Type :=
 c : nat -> Stream -> Stream.

CoFixpoint dummy (n:nat) : Stream :=
(* compute a streams of zeros, in a costly way. *)
 c (n*n - (n-1)*(n-1) - (2*(n-1)) -1) (dummy (n+1)).

Fixpoint get (n:nat) (s:Stream) {struct n} : nat :=
 match n,s with 0, c x _ => x | S p, c _ s => get p s end.

Definition dummy1 := dummy 1.
Time Eval vm_compute in get 300 dummy1.
(* Notice that computing up to the value 300 takes a long time (a few 
(3?) seconds) *)
Time Eval vm_compute in get 301 dummy1.
(* Notice that computing the next value takes almost no time: the stream 
is not
  recomputed, but computation is re-started from where we were before. *)
Time Eval vm_compute in get 300 (dummy 1).
(* Not a memo-function: the new "dummy 1" is not recognized as the same 
as the
  previous one: computation takes 3 seconds on my machine. *)
Time Eval vm_compute in let e := dummy 1 in get 300 e + get 300 e.
(* this also takes 3 seconds. *)
Time Eval vm_compute in get 300 (dummy 1) + get 300 (dummy 1).
(* this takes 6 seconds, as I expected. *)

However, there is a cost in memory consumption.

Yves