Hacker News Reader

Comment by wyager | Hacker News Reader

>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.)

View on HN

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.

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.)

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 [1] https://pamiz.wordpress.com/2014/02/13/the-functor-of-infini...

Nitpick on both links. They say `alpha . beta = id = beta . alpha`. This is wrong: `alpha . beta` composes to a different `id` from `beta . alpha`.

Reply on news.ycombinator.com