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 this1:

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

1 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

4 comments:

  1. As far as I can tell, it would be unsafe to put catch and handle out of IO, because Haskell exceptions are imprecise. The same pure value could evaluate to any number of results depending on which of the possible exceptions was raised this time. (And getting precise exceptions in the presence of laziness doesn't seem easy.)

    This is how the conflation of errors and non-termination is usually justified, because they can't be distinguished by pure code.

    Of course they're actually different things and they can be distinguished in the IO monad, but do we also want to give 10000 and "sum (replicate 10000 1)" a different denotation because they can be distinguished by impure code?

    ReplyDelete
    Replies
    1. As far as I can tell, it would be unsafe to put catch and handle out of IO, because Haskell exceptions are imprecise. The same pure value could evaluate to any number of results depending on which of the possible exceptions was raised this time.

      Imprecision isn't a safety problem (unless an optimizer mistakenly assumes that unspecified behavior is predictable); it's just less tractable (perhaps enough to qualify as impure, depending on the definition of "impure"). There are already implementation-dependent return values, so implementation-dependent choice of exceptions isn't much of a novelty. (Maybe I should have put that part of the post up front rather than in a footnote, because you're not the only reader to think I didn't know about imprecise exceptions.)

      (And getting precise exceptions in the presence of laziness doesn't seem easy.)

      Laziness alone isn't a problem - denotations can be evaluated lazily regardless of whether they're exceptions or returns. It's unspecified argument evaluation order that's the big annoyance — in languages which specify it, exceptions aren't implementation-dependent.

      Of course they're actually different things and they can be distinguished in the IO monad, but do we also want to give 10000 and "sum (replicate 10000 1)" a different denotation because they can be distinguished by impure code?

      Exceptions can communicate useful information (and it's reasonable for pure code to use that information), so different exceptions are different in a more meaningful way than different ways to compute the same result.

      Delete
  2. We very carefully do not say which _|_ you get when there are several that an expression could evaluate to.

    This can arise in the case that multiple values that we are strict in in an expression would each evalute to a different bottom.

    This enables the compiler to freely interchange the order of many operatons. It also has correctness implications for the very machinery used to evaluate the STG in parallel haskell, which may non-deterministically change whether something was detected as a loop but 'catch it on the backswing' due to lazy blackholing and the occasional miss in greyholing causing a thunk to evaluate twice. Spackling over these cases requires some _very_ expensive operations in terms of cycle count that would basically destroy the entire parallel RTS.

    Moving these exception handling bits outside of IO would make such shenanigans unsound. We'd have to lock down to an overly specified semantics with rigorous ordering, at the expense of a huge amount of possible parallelism and optimization or else pure code could start having differing results depending on the load of the machine or activity of the garbage collector!

    Non-termination is sometimes catchable in Haskell, but not always. We can often catch it when we loop around and find that computing the currently demanded answer requires us to evaluate the same thunk, but that isn't every non-termination, and we can often detect a different subset of them when working interactively than in compiled code.

    By moving the act of catching the exception out to the IO monad this non-determinacy is put in a place where it can't affect the pure fragment, which so long as it doesn't force an exception-inducing bottom will now always produce a consistent result, and equational reasoning is maintained.

    Also, exceptions in a lazy language can happen long after you'd expect them to. Which pure handler should be invoked? The one that lexically enclosed the exception where it was thrown in the code? or the one for the stack you are on when you forced it? This sorts of issues is why things like the blame calculus don't work in a lazy setting -- there isn't a right answer that works for all usecases.

    ReplyDelete
    Replies
    1. parallel haskell, which may non-deterministically change whether something was detected as a loop

      This is what I was missing. Optimizations and nondeterministic concurrency can cause variation within a single implementation, which is worse than variation between implementations, so it might belong in the sin-bin even though it's not unsafe or stateful or otherwise undenotational. Whether determinism is worth losing exception handling is debatable, but it's a better reason than hiding implementation-dependent behavior. (In a language that distinguished more than two purity levels, this would be less of an issue.)

      Non-termination is sometimes catchable in Haskell

      Wow, I had no idea actual implementations sometimes detected nontermination (except for deadlocks in some databases). I thought this was a theoretically possible feature that no one bothered with, since even when it works, an infinite-loop exception isn't a huge improvement on an infinite loop.

      Also, exceptions in a lazy language can happen long after you'd expect them to. Which pure handler should be invoked? The one that lexically enclosed the exception where it was thrown in the code? or the one for the stack you are on when you forced it?

      For denotational reasoning reasons, shouldn't the handler depend only on how the denotation is used, not on when it's computed? There could also be catch operations with non-denotational scopes (and thus implementation-dependent effects), but they should probably affect only exceptions not caught by a denotational catch.

      Delete

It's OK to comment on old posts.