It seems to be well-known that programming languages can't have sums, products and nontermination together.
Q1. Is this true? Below (or in the above link I gave) is a partial argument.
However, Hinze's Generic programming with Adjunctions ignores the issue, even after discussing somewhat precisely which is the involved category. In particular, he talks (seemingly without reservations) about Haskell being modeled by the category $\mathbf{SCpo}$ of strict continuous partial orders and having sums and products. But we know that Haskell does not have sums (right?). (Part of the paper uses $\mathbf{Set}$ instead, but that doesn't allow for non-termination).
Q2 So, what am I missing? I see four options:
- People often ignore non-termination on purpose when discussing Haskell. Perhaps this paper does it too. But why would one mention CPOs then?
- The barrier I discuss can be avoided in clever ways. In particular, the paper models non-strict Haskell functions $f : A \to B$ by strict functions $f : A_{\bot} \to B$, for other reasons.
- The paper does mention the limitation and I missed that. I've spent some effort looking for this mention and failed to find any.
- This is an actual mistake, and as everybody keeps claiming Haskell indeed lacks categorical sums (as other people agree on), even though the paper claims
Either
is such a thing. Everything works out nicely instead in total languages with inductive and coinductive types.
Background
It's well known that, in a bicartesian closed category (BCCC), if the initial and final object coincide (that is, if the category has a zero object) the category collapses (with all types being isomorphic) by $A \cong A \times 1 \cong A \times 0 \cong 0$ for all $A$.
This means, for instance, that the category of pointed sets, with its zero object, can't be bicartesian closed.
But the category SCpo also has a zero object for the same reason: all objects are structured sets (CPOs) with a bottom element $\bot$, and arrows are strict (and ($\omega$-)continuous) functions, so they preserve $\bot$. Indeed, this is attributed to Smyth and Plotkin (1982), who describe this category as $\mathbf{CPO}_{\bot}$ and state it lacks categorical products; other categories they consider lack other features of a BiCCC (e.g., their $\mathbf{CPO}$ lacks sums).
What is not clear to me is whether every way of handling $\bot$ falls into this trap. However, knowledgeable people on Reddit seem to repeat this claim without good sources (Filinski's master thesis was the best reference I got, and it doesn't lay out a generic categorical argument).