Roman Leshchinskiy wrote:
Ross Paterson wrote:
Hence I think the name should include the elements Data, List and Coinductive (or Unfold as suggested by Malcolm).
I have to disagree here. Our streams can be used to model both inductive (i.e. tail-strict) and coinductive lists. What data structure is being modelled is not a property of the Stream data type but rather of the stream operations. For inductive data types, we just have to make sure that streams are always fully consumed.
Every inductive (=finite) list is also a coinductive (=potentially infinite) list but not vice-versa. So it's trivially true that if streams model coinductive types, they can also model inductive ones (in a language with _|_ that is, otherwise fold couldn't be expressed). Regards, apfelmus