winterkoninkje | Idle musings on CPPOs (Reply)

I was thinking recently about the design of a language which makes pointedness explicit in the type theory. That is, there are benefits to working in provably-total languages, especially when it comes to the equivalence theorems you can prove; however, there are also benefits to working in non-total languages (namely, not needing to prove totality). Previous approaches to this sort of thing have been based in domain theory; in particular, they've been based on pointed cpos (cppos)— i.e., a cpo with a least element, representing the total lack of information, which is often conflated with nontermination. But there's a problem with this.

The problem is, there are some cpos which have a least element (and hence are technically cppo) but where that least element cannot or should not be conflated with nontermination. In particular, product domains are formed by the tupling of elements from various domains. Thus, given A = \Pi_{i \in I} B_i, if all the B_i are cppo then it follows that A is cppo: the least element of A is the tuple taking the least element of each of the B_i domains. However, the least element of A is not nontermination— it's a tuple (whose components may be nonterminating). That is, we can perform eta expansion of A, without running into the various issues that arise for Haskell's tuples. In the limit we can consider the product of the empty family of domains (aka, the domain with a single uninformative value), and this should not be confused with the result of lifting the empty domain (aka, the domain with a single non-terminating "value").

So clearly, if we are to use domain theory to reason about termination, we must distinguish cppos which are pointed by nontermination, vs cppos whose least element is eta-expandable. However, I'm not sure that this distinction has been made before in the literature...