The Coq mailing list

[roconnor AT theorem.ca]

On Sun, 26 Apr 2009, Bruno Barras wrote:

> Hi,
> Just 2 little remarks. Firstly, you don't have to go that far in the CPS 
> transformation, by adding the continuation only to map' (and not in the 
> stream' type). The most noticeable change w.r.t. Edsko's code is the type of 
> map':
>
> Definition map' (A B : Set) (f : A -> B)      (rec : (A -> B) -> stream A -> 
> stream B)
>     (xs : stream' A) (C:Type) (K : stream' B -> C) : C :=
>   match xs with
>   | inl u => K (inl _ u)
>   | inr (x, xs') => K (inr _ (f x, rec f xs'))
>   end.
> CoFixpoint map2 (A B : Set) (f : A -> B) (xs : stream A) : stream B :=
>   map' f (@map2 A B) (fromStream xs) toStream.
>
> (I haven't checked the example, but if it fails to type-check, this can be 
> fixed easily.)

I just checked and it works.  The key is that you put the continuation K 
into each branch of the match statement.  Very clever.  I'll try to 
remember this trick.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''