Partial list ($x_1:\cdots :x_n:\perp$)

A list whose spine or elements may contain bottom values. The displayed value has a known finite spine prefix and an undefined tail. An entirely undefined list exposes no outer constructor, while [] exposes a terminating empty list. These distinctions matter to strict functions and to the fold factorisation criterion.

No generic sequential pure Haskell operation can guarantee emission of every available input occurrence when either of two input spines may be the bottom value. To obtain an arbitrary element, it must eventually demand one input. That input can be undefined while the other is a defined singleton, so the demand blocks the promised singleton output. Choosing the other input first reverses the counterexample. Lazy evaluation cannot determine which computation will diverge; the positive two-stream fairness result needs proper lazy lists or a stronger concurrent computational model.

A finite list prefix followed by bottom records only the constructors known so far. The chain $\perp ,x_1:\perp ,x_1:x_2:\perp ,\dots$ approximates an infinite lazy list. A Scott continuous map is determined on the limit by its values on these approximations. This justifies extending an identity proved on finite partial lists to definable operations on infinite lists; equality merely on finite terminating lists does not provide the same premise.