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
?