I'm refining my understanding of the connection between initial algebras and datatypes. This paper suggests that one could even represent the categories corresponding to datatypes definitions:
as follows:
Where $1$ is the terminal object of the category.
My question is, how can I justify that $1$ is the terminal object of the category? Do I have to postulate that any type has a unique morphism to $1$? This morphisms would be different that the datatype definitions which would not be nice...
An empty product is the same thing as a terminal object by definition of the product: it's an object $1$ such that for every object $A$, there is a unique morphism $1_A : A \rightarrow 1$. ($1$ is a product of a family indexed by an empty set iff there exists an empty family of morphisms such that for every object $A$ and every empty family of morphisms, there is a morphism $1_A : A \rightarrow 1$ satisfying an empty family of properties.)
An empty product has a simple computational interpretation: it's a type with a single element. Haskell writes () for both the type and its value. ML calls the type unit and the value (). A function whose interpretation is $1_A$ is a constant function taking an object of type $A$ as its argument and returning the value () of type $1$. It's the only total function of this type.
Likewise an empty coproduct $0$ is an initial object: an object such as for every $A$ there is a unique morphism $0_A : 0 \rightarrow A$. The computational interpretation is an empty type. Writing a function whose denotation is $0_A$ is tricky: most programming languages don't allow it without using features that don't fit well in a simple categorical semantics such as exceptions or recursion.
When you're building the categorical semantics, you do need to define everything, including “trivial” cases like terminal objects. You can't just assume that one exists. To give a concrete example, if you take a simple subset of the types of the C programming language allowing only basic types such as int and char and compound types built with struct, you can build binary products using struct, but you cannot build an empty product, because C forbids objects of size 0 and an object whose type is an empty struct would have the size 0.
