Consider the Haskell-style data type:
\textbf {data}\ \mathit {Bin} = \mathsf {Zero}\ \mathit {Bin} \mid \mathsf {Empty} \mid \mathsf {One}\ \mathit {Bin}
So, e.g. \mathsf {One}\ (\mathsf {Zero}\ (\mathsf {One}\ \mathsf {Empty})) : \mathit {Bin}.
The recursive domain equation is, expressed as a fixed point:
B \simeq \mathcal {F}(B)\quad \text {where}\ \mathcal {F}(X) = X + \mathbf {1} + X
We wish to show that \mathcal {F} is a cocontinuous endofunctor.
We have a mapping \mathcal {F} on cpos (objects of the category \textbf {Cpo}), but for it to be a functor we additionally need a mapping \mathcal {F} on continuous functions (morphisms of the category \textbf {Cpo}).
Recalling our sum construction, we may remember that sums are already a bifunctor \textbf {Cpo} \times \textbf {Cpo} \rightarrow \textbf {Cpo} (Theorem [dt-0038]). Thus, our mapping on continuous functions \mathcal {F} can be derived from our mapping on cpos \mathcal {F} by using the morphism mapping from the sum construction (Definition [dt-0037]). Given a continuous function f : A \twoheadrightarrow B, our morphism mapping is:
\begin {array}{l}
\mathcal {F}(f) : \mathcal {F}(A)\twoheadrightarrow \mathcal {F}(B)\\
\mathcal {F}(f) \triangleq f + \mathsf {id}_\textbf {1} + f
\end {array}
Proof that this endofunctor is cocontinuous is left for the reader. Hence the semantics of the type \mathit {Bin}, i.e. \llbracket \mathit {Bin} \rrbracket : \textbf {Cpo} is the least fixed point of \mathcal {F}, i.e. the colimit of the \omega -chain:
Let us visualise this chain. Here the sum injections have been written as \textsf {Z, E, O} rather than (combinations of) \textsf {inl} and \textsf {inr} to keep the connection with the Haskell data type clear.
Thus, the nth cpo in the chain contains binary numbers with at most n defined digits. The colimit of the chain contains all binary numbers (finite, partial, and infinite!).
