In general, I don't think there is a "standard" definition of a stream datatype. IIUC, you see streams as necessarily infinite but there are other perfectly valid interpretations. Stream is simply a very broad term which means too many different things. In particular, I don't see why our Stream data type doesn't model streams.
I have to admit that, in general, "stream" can mean a lot of different things. A quick google gives all kinds of results, from streaming media to bandwidth benchmarks. However, there is quite a lot of research, closely related to functional programming, with a clear consensus of what a stream is: \nu X . A * X (or equivalently, functions from Nat -> A) Personally, I think this gives a very clear definition of what a stream is that leaves nothing open to interpretation. Of course people are free to call their data types whatever they like, but in this instance it may be advisable to at least be aware of any related work. Of course, your streams (what I would call colists) can be used to model this type. There are very compelling reasons not to do this: streams are a comonad, colists are not; streams and colists have are really different instances of Monad (just look at the definition of return for both cases); colists are a monoid, streams are not; I'm sure Conor can come up with plenty of other reasons. The important thing is, although you can model streams using colists (I'm using my terminology here), it may not be desirable to do so. It can sometimes pay to be as precise as possible about your types.
I have to admit that I don't really understand the distinction between Haskell's lists and colists (or, in general, datatypes in Haskell and codatatypes). To me, lists are inductive and colists are coinductive, i.e., the former are the least and the latter the greatest fixed point of the underlying functor. Thus, Haskell's list datatype actually models colists (and algebraic datatypes in Haskell are coinductive by default). This thread seems to implicitly assume a different interpretation of the prefix "co" but I don't really understand what this interpretation is.
That's exactly the way I think about this as well. In the context of Haskell, the distinction is not so clear. When you write "data" as a programmer, you sometimes really mean codata (as in my Stream type). On the other hand, there are occassions where you have an (implicit) invariant in your head stating you will never construct infinite terms, and hence it's safe to assume that a fold will terminate, for instance. Then you really mean data - and not codata. Haskell does not support this separation: both data and codata are introduced by the same language construct. It's a real pity sometimes; if we really care about the types of our programs, I think this is a distinction worth making. All the best, Wouter This message has been checked for viruses but the contents of an attachment may still contain software viruses, which could damage your computer system: you are advised to perform your own checks. Email communications with the University of Nottingham may be monitored as permitted by UK legislation.