Ross Paterson wrote:
On Tue, Nov 20, 2007 at 07:25:08PM +1100, Roman Leshchinskiy wrote:
Ross Paterson wrote:
I was saying that your "streams" are themselves coinductive objects. Is that controversial? They aren't recursive so in my view, they themselves are just as (co)inductive as, say, a function of type (a -> a).
To quote your own paper, "stream fusion uses an explicit representation of the sequence co-structure [or unfolding]: the Stream type." The key property of System F encodings is that they encode a recursive type in a non-recursive form, and Stream (ignoring Skip) is the standard System F encoding of co-inductive lists.
All true, but to me, there is a difference between encoding coinductive structure and being coinductive. After all, "encoding" is to a certain extent a matter of interpretation. Anyway, I guess we only disagree about terminology. Roman