Oversimplifying bottom

There are a few things that bother me about the usual treatment of ⊥ in Haskell culture:

Multiple failures

I'm uncomfortable with the practice of treating all failures as a single ⊥ value, since they're actually distinguishable. Haskell denotations (ignoring side effects and implementation-dependent behavior) look like this¹:

data Denotation = Return Value | Throw Exception | Nontermination

The traditional ⊥ combines the Throw and Nontermination constructors. Since catch/handle can distinguish different exceptions, these are actually many different denotations, not one.

This must be a standard objection. The obvious response is that the distinctions between bottoms are usually irrelevant, and ignoring them makes reasoning about programs easier, even if it does occasionally give incorrect results. This isn't consistent with usage in the Haskell community, though, because Haskellers use ⊥ most when they want rigor. Nor is it consistent with the rest of Haskell culture, which generally frowns on unsafe shortcuts.

Haskellers appear to be aware of this, but they usually ignore it. I suspect this is due partly to a distaste for denotations outside the Return branch — exceptions aren't “proper” values and don't deserve attention.

This does cause confusion. For instance, it leads ezyang, when discussing definedness monotonicity, to identify nonmonotonic functions as uncomputable, without mentioning that this applies only to nontermination, not to other bottoms. When he later discusses distinguishing between bottoms, he calls this “a very operational notion” and ignores the possibility of catching exceptions — perhaps because Haskell discourages this by putting catch and handle in IO, even though there's nothing impure or unsafe about them.

The bottom type and the bottom value

Haskell culture also traditionally conflates the failure ⊥ with the bottom type, i.e. the values that are members of every type. This is understandable, since they coincide in Haskell — but that's a quirk of Haskell, not a law of denotational semantics.

It happens to be the case in Haskell that failures are the only denotations found in every type. But this is because Haskell types describe only one of the three branches of the denotation. A Haskell type describes what values an expression might return, but says nothing about exceptions or nontermination. If Haskell types could also specify whether an expression might terminate, and what exceptions it might throw (as in Java and C++), then the bottom type would be empty. (And type inference would be undecidable, which is why Haskell doesn't do it.) Failures are in the bottom type only because Haskell's type system can't talk about them.

It's also possible for the bottom type to contain values that aren't failures. For example, if Java didn't have primitive types, its null would be a bottom value, since it's a member of every (static) type. But it's not a failure: there are still useful operations on it, e.g. ==. Nor is it a zero of most operations.

It's probably safe to identify these two bottoms when speaking only of Haskell, but it seems to me Haskellers often do so even when speaking of denotational semantics in general.

Weakness is strength?

I worry that the treatment of ⊥ stems from a pattern of treating Haskell's weaknesses as strengths, or as inevitable mathematical results, rather than as accidents of one language. For example, some Haskellers consider definedness monotonicity a virtue rather than a weakness. (Inability to handle errors makes it easy to prove that your program doesn't recover from them, but hard to make the program do so!) There might be something similar in attitudes to type system extensions, but I don't understand this area well enough to tell.

What do Haskellers (particularly denotationalists) think about this?

Added 6 Sep: Most of these issues (catch is impure, bottom type = bottom value, monotonicity) involve treating quirks of Haskell as universal, but the conflation of multiple bottoms is the reverse: people ignore part of Haskell's semantics in favour of a simpler approximation.

A long footnote about denoting denotations

¹ The usual definition of Haskell denotations is that of Peyton Jones et al. in A semantics for imprecise exceptions: to hide the effect of implementation-dependent evaluation order on exceptions (e.g. what exception does 1/0 + undefined throw?), failure denotations give not a single exception but a set of possible exceptions. In addition, nontermination is treated as an exception, so denotations look like this:

data Denotation = Return Value | Throw [Exception]

Since even return values can be implementation-dependent, I think it's cleaner to make the whole denotation a set of implementation-dependent results. Also, nontermination is quite different from exceptions, in both implementation and semantics: it's a zero of catch, so any attempt to detect it will also give Nontermination. (This is apparently not considered an important distinction in formal semantics, but it's very different operationally.) This gives a slightly more complicated definition:

data Result = Return Value | Throw Exception | Nontermination
type Denotation = [Result]

Actual implementations invariably pick one result, so the complexity of treating a denotation as a set of possible results is usually irrelevant and can be ignored, leaving this definition of a denotation-as-implemented:

data Denotation = Return Value | Throw Exception | Nontermination

If nontermination is treated as an exception, this becomes pleasingly conventional:

type Denotation = Either Exception Value