A bicartesian closed category of strict complete partial orders (Hask)

Question

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).

Answer 1

Yes, it's impossible to have a nondegenerate CCC with general recursion and categorical coproducts. The standard reference for this is:

H. Huwig and A. Poigne. A note on inconsistencies caused by fixpoints in a cartesian closed category. Theoretical Computer Science, 73:101–112, 1990.

However, I and (most of the other people I've met) learned about it from Achim Jung and Samson Abramsky's handbook chapter Domain Theory, which they have kindly made available for free.

Most of the categories of domains that people work with are subcategories of DCPO, the category of predomains and continuous functions on them. Since predomains do not necessarily have a least fixed point, this category is a bi-CCC, but fixed points only exist for functions into domains.

On page 46 of these notes, there is a big table telling you which subcategory of DCPO different constructions exist in.