Differences between List Colist and Stream

• A List is a finite datastructure containing multiple elements, possibly 0.
• a Stream is an infinite datastructure, it always produces elements when queried. This also means it contains at least one element.
• A CoList is a possibly infinite list of elements, possibly 0.

Definitions

data List a = Nil | (::) a (List a)

record stream (a : Type) where
  constructor (::)
  head : a
  tail : Inf (Stream a)

data CoList a = Nil | (::) a (Inf (Stream a))

So a List is a finite Colist and a Stream is an infinite CoList

Maybe CoList and Stream should be flipped so both List and CoList are derivable from Stream?