6 ms·

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 or

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. The solution in a lazy language like Haskell is to be specific about when things get forced, which outside of explicit overrides only happens in response to actual usage of that expression, eg. when the value is printed. At this point you're naturally forced to introduce either sequentialization or explicit parallelism; in the former there is no issue and in the latter you still need to explicitly sequence the results, of which the exceptions are a relevant part. In a strict language like Rust, of course, you never aimed to have this property anyway.

chriswarbo 9y ago
> 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 9y ago
  > 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 9y ago
    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 9y ago
      > 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.
      - 9y ago

chriswarbo 9y ago

> 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 9y ago
> 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 9y ago
  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 9y ago
    > 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.
    - 9y ago