4 ms·

The difference is not one of "philosophy", but rather of using the right types. Haskell's so-called "list" type constructor is actually a type constructor of st

The difference is not one of "philosophy", but rather of using the right types. Haskell's so-called "list" type constructor is actually a type constructor of streams. Unsurprisingly, streams are much better than lists if you want to do stream processing.

wyager 11y ago
>Haskell's so-called "list" type constructor is actually a type constructor of streams. Most papers consider streams to be lists without a terminal constructor. Haskell lists are a superset of streams. All streams have infinite lengths, but only some lists have infinite length. (Again, this just comes down to definition, but this is how most functional papers describe it.)
- catnaroek 11y ago
  In chapter 4 of his book, Okasaki defines a type of both finite and infinite streams (which is really just the type of Haskell "lists"), and, in the remainder of the book, he only uses finite ones. A stream of infinite length, which you call "stream" without qualification, is what I call "a function on the natural numbers". (Well, up to isomorphism.)
  - chas 11y ago
    Speaking of things that the Haskell type system lets you make explicit, the isomorphism between streams and functions from the natural numbers means that streams are "representable functors" in the jargon of category theory. [1] Knowing that a data type is representable allows you to immediately build a bunch of other interesting structures on the data type. [0] [0] http://covariant.me/notes/rep-functors.html http://covariant.me/notes/rep-functors.html [1] https://pamiz.wordpress.com/2014/02/13/the-functor-of-infinite-lists-is-representable-by-natural-numbers/ https://pamiz.wordpress.com/2014/02/13/the-functor-of-infini...
    - catnaroek 11y ago
      Nitpick on both links. They say `alpha . beta = id = beta . alpha`. This is wrong: `alpha . beta` composes to a different `id` from `beta . alpha`.
- tel 11y ago
  That's one way of doing it, but most formally I think it has to do with whether you're considering the list type in a "data" sense or a "codata" sense. In either case you might be talking about the same "shape" of data, but streams are defined under observation as compared to construction.

wyager 11y ago

>Haskell's so-called "list" type constructor is actually a type constructor of streams. Most papers consider streams to be lists without a terminal constructor. Haskell lists are a superset of streams. All streams have infinite lengths, but only some lists have infinite length. (Again, this just comes down to definition, but this is how most functional papers describe it.)

catnaroek 11y ago
In chapter 4 of his book, Okasaki defines a type of both finite and infinite streams (which is really just the type of Haskell "lists"), and, in the remainder of the book, he only uses finite ones. A stream of infinite length, which you call "stream" without qualification, is what I call "a function on the natural numbers". (Well, up to isomorphism.)
- chas 11y ago
  Speaking of things that the Haskell type system lets you make explicit, the isomorphism between streams and functions from the natural numbers means that streams are "representable functors" in the jargon of category theory. [1] Knowing that a data type is representable allows you to immediately build a bunch of other interesting structures on the data type. [0] [0] http://covariant.me/notes/rep-functors.html http://covariant.me/notes/rep-functors.html [1] https://pamiz.wordpress.com/2014/02/13/the-functor-of-infinite-lists-is-representable-by-natural-numbers/ https://pamiz.wordpress.com/2014/02/13/the-functor-of-infini...
  - catnaroek 11y ago
    Nitpick on both links. They say `alpha . beta = id = beta . alpha`. This is wrong: `alpha . beta` composes to a different `id` from `beta . alpha`.
tel 11y ago
That's one way of doing it, but most formally I think it has to do with whether you're considering the list type in a "data" sense or a "codata" sense. In either case you might be talking about the same "shape" of data, but streams are defined under observation as compared to construction.