[chriswarbo]

> The issue here seems to have little to do with exception handlers; see that

> head [0, throw E]

> also produces such an "indeterminate" answer depending on order of evaluation, as long as you define things as you have here.

I disagree; note that I said:

> we treat an "unhandled exception" as not getting an answer (equivalent to an infinite loop)

More formally, throwing an exception/error results in _|_ (bottom) and all _|_ results are equivalent i.e. we can't tell "which error" we got. In particular, we can't tell the difference between _|_ due to an error being thrown, and _|_ due to an infinite loop.

This is important in a general recursive language, since we can't know (in general) whether evaluating some value (with whatever strategy) will eventually produce a result or not. Consider the following, where omega = (\x -> x x)(\x -> x x):

    head [0, omega]

Under a call-by-name strategy this will reduce to 0, under call-by-value it will loop forever, i.e. giving _|_. Should this count as breaking confluence?

Total languages like Agda and Coq would say this breaks confluence, due to general recursion being a side-effect, and hence it should be encoded as such rather than allowed willy-nilly.

Turing-complete languages like Haskell would say that such encoding is cumbersome, and hence that their notion of confluence should be weaker; specifically, evaluating an expression using any evaluation strategy to get a value other than _|_ will produce the same value.

It just so happens that lazy evaluation has the property that if some (perhaps unknown) strategy can reduce an expression to normal form, then non-strict evaluation can also reduce it to normal form. In other words, lazy evaluation avoids all 'avoidable' infinite loops, but it still gets stuck in 'unavoidable' ones. That's nice, but isn't important for confluence.

You're perfectly right that introducing sequencing like `seq` throws a spanner in the works :)

[Veedrac]

> throwing an exception/error results in _|_ (bottom) and all _|_ results are equivalent

My point is that they're not when you have `catch`, and that this distinction adds nothing that ⊥ doesn't already add with regards to order of evaluation.

[chriswarbo]

I'll have to think about this some more, since I don't quite understand.

Let's say we have the following Haskell definitions:

    error msg = undefined  -- "throwing an error"
    undefined = undefined  -- infinite loop

In this setup, there's no way for us to tell, under any evaluation strategy, whether or not an expression evaluates to _|_. Any code we might write to "check" for this would have to run "after" an infinite loop, which is impossible. Hence it's impossible to write an expression which, under any evaluation strategy, normalises to two distinct non-_|_ values: either it always produces the same value, or it sometimes produces one value and sometimes _|_ (depending on the strategy), or it always produces _|_ regardless of strategy.

If we can distinguish between "different _|_s", e.g. catching some as exception values, then we can write an expression which reduces to different non-_|_ values depending on the evaluation strategy, and hence we lose confluence (the weaker form; we already lost the stronger Coq/Agda form by having _|_ in the first place).

This is fundamentally different to the value-or-_|_ uncertainty, since that's unobservable from within the language.

[Veedrac]

> This is fundamentally different to the value-or-_|_ uncertainty, since that's unobservable from within the language.

This seems to be a much weaker claim than I thought you to be making; of course being able to catch errors moves visibility of errors from externally visible to internally visible. That's the goal, after all.

I disagree, however, that this matters in the regards you raise, because a language which can arbitrarily decide to return ⊥ on the basis that it isn't internally visible is a broken language and any reasonable implementation needs to avoid that.

[chriswarbo]

You're right that having some mechanism to act gracefully in the case of errors is almost always required. "Internally" this might be a "main loop" with an exception handler. "Externally" this might be a bash script which runs our binary in a loop, or a systemd service, etc.

The intriguing thing about Haskell's approach is that it shows us that such mechanisms aren't pareto-improvements: we have to give up something, like confluence.

Keep in mind that confluence isn't just academic, it's the thing which makes functional programming attractive for parallelism. Confluence solves the hard problem of taking all possible interleavings of concurrent execution into account, since they act like different evaluation orders, and hence can't mess up the result.

Servers are a scenario where these two features clash: we want concurrency and parallelism for scaling, but we need restart loops to prevent downtime.

The use of external restart loops reminds me of delimited continuations, where even "undelimited continuations" are still delimited by the OS (e.g. Scheme's current continuation doesn't include the state of other OS processes). Likewise, "unobservable errors" can still be observed by the OS (e.g. when our process dies, as in a bash or systemd loop).

I think a good compromise is to "stratify" error handling: we write our business logic (or whatever) in a provably confluent sub-set of our language, and execute that logic using non-confluent features like error handlers. Confluent expressions can take advantage of optimisations (e.g. speculative evaluation) which are invalid for the wrapper.

One thing I'm not sure about is nesting exception-handling code in pure code. Approaches like algebraic effect systems let us mark expressions as requiring effects like 'stdio', yet we can handle those effects in a pure way (e.g. using hard-coded strings during a test). I don't think this is enough to maintain confluence in the face of concurrency though; we'd probably have to pass in a deterministic scheduler, but that may parallelism gains of things like speculative evaluation, work-stealing, etc.

[Veedrac]

> You're right that having some mechanism to act gracefully in the case of errors is almost always required. "Internally" this might be a "main loop" with an exception handler.

This isn't (just) about exceptions that escape; you also need to guarantee that fst (0, ⊥) returns 0 rather than ⊥. Heck, you're practically required to do the same for

    fst (0, [0..(10 ^ 10)] !! (10 ^ 10))

and for that evaluation order isn't even visible at the denotational level.

> Keep in mind that confluence isn't just academic, it's the thing which makes functional programming attractive for parallelism.

Automatic parallelisation of functional languages is academic.

[chriswarbo]

> you also need to guarantee that fst (0, ⊥) returns 0 rather than ⊥

Why guarantee 0 instead of ⊥? I'd say it's due to a general agreement that ⊥ has the lowest desirability: if we have the option of returning ⊥ or something else, we should pick that something else. Non-strict evaluation strategies are the most extreme choice, but most languages consider the desirability of strictness to be stronger than than the undesirability of ⊥.

I don't think exceptions are so simple though. Imagine a situation like this:

    getUserById :: [UserDetails] -> UserId -> User
    getUserById db id = MkUser id (getName details) (getDOB details)
      where details = head (filter ((== id) . getID) db)

On one hand, we may want this to fail fast: if `head` throws an `EmptyList` exception, we want to propagate that to the whole expression. Since getUserById might throw, we can wrap it in exception handlers and deal with missing users appropriately.

On the other hand, we may want to ignore exceptions in sub-expressions that we don't care about, e.g. having `fst (0, Exception)` reduce to 0. This seems trickier for `getUserById`, since we might do a bunch of processing which only needs the ID, and end up triggering the `EmptyList` exception far away, deep in the heart of a pure-looking function. I can think of three solutions to this:

- Wrap exception handlers around the subsequent steps. This smells funny, since those steps might be completely pure.

- Jump back to the original exception handler. Such non-local jumps may be very hard to understand, plus the handler would need to work in arbitrary contexts; all it can really do is return a different value of the same type (e.g. some predetermined default), or throw a different exception (which just defers the problem) or produce ⊥.

- Mark potentially-exceptional values somehow, so we can track their propagation through the program, and handle them if needed. That doesn't seem any different than `Maybe` or `Either`, perhaps modulo some lifting.

Of course, the situation becomes even more complicated if an expression contains many different exceptions!

> Automatic parallelisation of functional languages is academic.

Note I said "attractive", not "automatically solves all problems" ;) Even with "manual" parallelism, like `par`, map/reduce, etc. it's nice that these don't alter the semantics.

It also simplifies compiler optimisations, and helps programmers reason about when they will/won't fire.