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