Consider the following datatype:
data Foo = Halt | Iter Foo
This is the fixpoint of Maybe
. It contains the direct limit of the sequence Void
, Maybe Void
, Maybe (Maybe Void)
and so on, where pure
is the injecting morphism. However, Foo
has an element not covered by the direct limit, namely fix Iter
.
Let me have another example:
data Bar = Bar Bar Bar
This is the fixpoint of Complex
. Since Void
, Complex Void
, Complex (Complex Void)
and so on are all homeomorphic to Void
, the direct limit is also Void
. However, Bar
has an element, namely fix (join Bar)
.
So what's the mathematical justification of those "leftover" elements?
As was pointed out in the comments, these elements exist as a consequence of nontermination.
In a terminating language, or equivalently, in the category of sets, the initial algebra (least fixed point) of Maybe
is Nat
and the initial algebra of Complex
(data Complex a = Complex a a
) is the empty type Void
. fix Iter
and fix (join Complex)
don't exist because fix
is not definable in a terminating language.
With unrestricted nontermination, sets are no longer a good model of types because the infinite loop inhabits all types. A common alternative in that case are DCPOs or some similar order structure. In particular, the existence of bottom and of limits for increasing sequences are just what is needed to be able to define fix
(via Kleene's theorem). So for example, in the case of data Nat = Z | S Nat
, fix S
is obtained as the limit of the sequence ⊥
, S ⊥
, S (S ⊥)
, S (S (S ⊥))
, etc.
You do need to be careful about where the bottoms are. For example, in Haskell, Maybe a
is a DCPO consisting of ⊥
, Nothing
, and Just x
for x
an inhabitant of a
. You can also define a strict variant:
data SMaybe a
= Nothing
| Just !a
which as a DCPO contains ⊥
, Nothing
, and Just x
for x
a non-bottom inhabitant of a
. In particular, the sequence ⊥
, Just ⊥
, Just (Just ⊥)
, etc. is no longer well-defined (or if you really want to give it a value, it would be constantly equal to ⊥
), so you no longer get a way to construct an infinite sequence of Just
, and indeed the initial algebra (least fixed point) of SMaybe
only contains finite sequences of Just
/S
applied to Nothing
/Z
, and ⊥
alone.
Note that this is not restricted to lazy languages. DCPOs serve just as well to model strict languages. It's just that there is an explicit distinction between values and computations which makes things more obvious in a way. For example, the option type in ML
type 'a option = None | Some of 'a
corresponds to the set of values consisting of None
and Some x
for x
in 'a
. But the type unit -> 'a option
is not a pure function from unit
values to 'a option
values. It is a function from unit
to computations with result 'a option
. A computation with result type t
denotes an element of the lifted type {⊥} + t
(i.e., either bottom or a value in t
). So you can use unit -> _
as a type of thunks and encode everything that's going on in Haskell in a strict language.