Exception vs Result

Learning
1

Last week, @BikalGurung blogged On Effectiveness of Exceptions in OCaml, in part as a follow-up to his announcement of his parser combinator library reparse, which eschews Result-based error handling in favor of exceptions. I’ve long preferred using Result (and its equivalents in other languages), and my experience so far with OCaml is that that preference is shared by many in the community and by authors of key libraries, but I was happy to consider a new counterpoint.

Doing so prompted me to consider my rationale(s) more than I had previously, and do some additional reading and research, all of which ended up further cementing my pro-Result bias. What follows are counterpoints to Bikal’s two most consequential arguments (in my opinion), and some elaboration beyond. Many thanks to Bikal for his posting his experience report!

Stacktrace / Location Information

First, Bikal focuses in on how useful error handling should “allow us to efficiently, correctly and accurately identify the source of our errors”. I agree, but he compares exceptions and result on this basis like so:

OCaml exception back traces - or call/stack traces - is one such tool which I have found very helpful. It gives the offending file and the line number in it. This make investigating and zeroing in on the error efficient and productive.

Using result type means you lose this valuable utility that is in-built to the ocaml language and the compiler.

It is true that Error does not implicitly carry backtraces as exceptions do, but there is nothing preventing one from choosing to include a backtrace with a returned error, since OCaml backtraces helpfully exist separate from its exception facility:

let b x =
  if x > 0
  then Ok 0
  else Error ("unimplemented", Printexc.get_callstack 10)

let a x = b x

let _ = match a (int_of_string @@ Sys.argv.(1)) with
          | Ok v -> Format.printf "%d@." v
          | Error (msg, stack) ->
            Format.fprintf Format.err_formatter "Error: %s@." msg;
            Printexc.print_raw_backtrace stderr stack

$ ocamlc -g -o demo.exe src/demo.ml 
$ ./demo.exe -1
Error: unimplemented
Raised by primitive operation at file "src/demo.ml", line 5, characters 31-56
Called from file "src/demo.ml", line 9, characters 14-47

From a strictly ergonomic standpoint, it makes sense to wish that e.g. the Error constructor were treated specially such that values it produced always carried a stack trace (as exceptions do/are), so that programmers would not need to opt into it as above. However, that would not come without costs, including a maybe-significant runtime penalty that might render Result a less useful way to cheaply signal recoverable error conditions (something that other exception-dominant languages/runtimes struggle to do given that stacktrace generation is far from free).

Correctness

Bikal’s final topic was re: correctness, and to what extent using one or another error-handling mechanism tangibly affects his work. What he says is short enough to reproduce in full:

I thought this would be the biggest advantage of using result type and a net benefit. However, my experience of NOT using it didn’t result in any noticeable reduction of correct by construction OCaml software. Conversely, I didn’t notice any noticeable improvement on this metric when using it. What I have noticed over time is that abstraction/encapsulation mechanisms and type system in particular play by far the most significant role in creating correct by construction OCaml software.

There’s a lot left undefined here: what “correct by construction” might mean generally, what it means in the context of OCaml software development, how it could be measured (is there a metric, or are we just reckoning here?), and so on.

While reminding myself of exactly what “correct by construction” meant, I came across a fantastic lecture by Martyn Thomas[1] that neatly defines it (and goes into some detail of how to go about achieving it); from the accompanying lecture notes[2]:

…you start by writing a requirements specification in a way that makes it possible to analyse whether it contains logical omissions or contradictions. Then you develop the software in a way that provides very strong evidence that the program implements the specification (and does nothing else) and that it will not fail at runtime. We call this making software “correct by construction”, because the way in which the software is constructed guarantees that it has these properties.

While we aren’t working with anything as formal as a theorem prover when we are programming in OCaml, it does provide us with a tremendous degree of certainty about how our programs will behave. One of the greatest sources of that certainty is its default of requiring functions and pattern matches to be exhaustive with regard to the domain of values of the type(s) they accept; i.e. a function that accepts a result must provide cases for all of its known constructors:

let get = function Ok v -> v

$ ocamlc -g -o demo.exe src/demo.ml 
File "src/demo.ml", line 15, characters 10-28:
15 | let get = function Ok v -> v 
               ^^^^^^^^^^^^^^^^^^
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
Error _

This one way we “provide evidence” to the OCaml compiler that our code does not not contain “logical omissions”, to use Prof. Thomas’ nomenclature.

There are ways to relax this requirement, though. Aside from simply telling the compiler to not bother us with its concerns via an attribute:

let get = function Ok v -> v [@@warning "-8"]

…we could simply use exceptions instead. For example, an exception-based variant of the program I started with earlier:

exception Unimplemented

let a x =
  if x > 0
  then 0
  else raise Unimplemented

let _ = Format.printf "%d@." @@ a (int_of_string @@ Sys.argv.(1))

This approach is less correct by any measure: the Unimplemented exception is not indicated in the signature of a, making it easy to call a without handling the exception, or being aware of its possibility at all. Insofar as the exceptions in question are not intended to be fatal, program-terminating errors, this approach absolutely increases the potential for “logical omissions”, increases the potential for programs to fail at runtime, and hobbles the exhaustivity guarantees that the OCaml compiler provides for us otherwise.

Later in the reparse announcement thread, @rixed said (presumably in response to this tension):

If only we had a way to know statically which exceptions can escape any functions that would be the best of both worlds!

And indeed, this approach of incorporating known thrown exception types into function signatures is a known technique, (in)famously included in Java from the beginning (called checked exceptions), but widely disdained. I suspect that disdain was more due to Java’s other weaknesses in exception handling than the principal notion of propagating exception types in function/method signatures. It would be interesting to see something like checked exceptions experimented with in OCaml, though it may be that doing so would nullify one of the primary benefits that those preferring exceptions enjoy (perceived improved aesthetics/clarity), and/or the work needed to achieve this might approximate the typed effect handling approaches that @lpw25 et al. have been pursuing for some time.

[1]: Making Software ‘Correct by Construction’ https://www.gresham.ac.uk/lectures-and-events/making-software-correct-by-construction
[2]: https://www.gresham.ac.uk/lecture/transcript/download/making-software-correct-by-construction/

12 Likes
2

Just chiming in to note that there has been an interesting discussion on this topic two years ago: Specific reason for not embracing the use of exceptions for error propagation?

It’s also interesting to note that that discussion also ended up talking about typed effects.
As I understand it, they would indeed subsume checked exceptions, and I’m quite excited about them.

2 Likes
3

Yes, thank for linking to that. There are actually a half-dozen relevant threads on this forum (and some in stackoverflow) on this topic, but I didn’t want to either blindly dump them all in the post, or try to write around them. :slight_smile:

The main insight for me that I hadn’t considered explicitly before was that the transformation of a function from returning a result to potentially throwing an exception is equivalent to eliding a compiler error on a nonexhaustive pattern match. The consequences for correctness are…notable?

1 Like
4

I think it depends on the use case. In rust and other languages, you have a distinction between recoverable (result) and unrecoverable (panic) errors. In some fields most errors will be unrecoverable: if you write a compiler or a theorem prover, exceptions are nice because there’s not much you can do if things fail imho. In other cases, you may have a lot of IO errors where you can retry on error.

At API boundary I think result is generally better in 2020, it documents better. Within a program I’m not always convinced it’s better.

9 Likes
5

I’m going to address the general issue of “programming with monads”, and not specifically the result monad, b/c I think it’s just an instance of the general phenomenon.

TL;DR In 1992, when someone told me about “programming with monads”, I replied that I already programmed with monads: I used the “SML Monad”. And this LtU post seems to me to be pithily succinct ( Are Monads a Waste of Time? | Lambda the Ultimate )

(1) when we talk about program correctness, we mean two things: reasoning about programs, and type-safety. I’ll address each in turn below.

(2) All monadic transformations of which I am aware (exceptions, state, control, I/O) are direct equivalents to the “standard semantics” for such language-features, e.g. as described in Michael J.C. Gordon’s book The Denotational Description of Programming Languages. Programming with monads is programming with some combinators and macros, on the right-hand-side of the denotational interpreters in that book.

(3) “reasoning about programs” has historically meant “equational reasoning”, and IIUC, Felleisen&Sabry’s work (and follow-on works) proved pretty conclusively that anything you can prove about the right-hand-side of the denotational semantics interpeter defiition, you can “pull back” to equational reasoning with extra rules, on the left-hand-side of the DS interpreter.

(4) “type safety”:

If only we had a way to know statically which exceptions can escape any functions

There was a cottage industry of “effect type systems” to capture/reason-about exceptions, state, maybe other things, decades ago. They were judged too cumbersome for programmers to use, and hence died-out. >10yr ago there was a caml-light (OCaml?) variant that checked exceptions in function-types; it didn’t catch on. Look at Java, where some exceptions are “checked” and others are not: some exceptions, it’s just too cumbersome to track in the type system. And so either your “result” monad only captures some of the exceptions, or it’s going to be wildly cumbersome.

(5) Monads are less-efficient than direct-style, memory-wise. For me, the moment in 1992 when I (an avowed SML/NJ bigot) became convinced of the superiority of caml-light (notwithstanding 2.5x slower on average) was when I realized that it was -so- much less memory-intensive. Because it didn’t allocate stack-frames on the heap, and closures started out on the stack and only moved to the heap on-demand. Henry Baker made the observation >20yr ago that the stack is a form of nursery. Writing in monadic style is sacrificing this obviously performance advantage. In the era of multicore, arguments made back then about memory, can be recast as arguments about the cache today, since (as hardware designers put it) “memory is at infinity” today.

P.S. And yet, I use monads sometimes, too. Rarely. But for instance, it’s a good model for (e.g.) writing a type-checker that wants to type-check a list of expressions (no unification, hence no side-effects) and not stop at the firs type-error, but rather gather together errors from all the expressions in the list, and produce an error with all of them combined. So the type-checker at the top of each member of the list catches any raised exception, stores it in an accumulator, and goes on to the rest of the list; at the end of the list, if the accumulator is empty, it returns the list of result-types; otherwise it raises an exception containing list of errors stored in the accumulator.

It’s rare, and if the Result monad didn’t exist, I’d hack something together, but … it’s literally the only use I can think of, that wasn’t driven by a library (e.g. bos) using the Result monad itself (and my needing to use that library).

And this efficiency is the real reason that exception-based backtraces are better: IIUC, OCaml exceptions are really cheap because they don’t materialize that backtrace until demanded. It means that you have to be careful what code you put between the “try-with” and the demand for the backtrace, but it’s efficient. Materializing the backtrace for every exception raised would be … pretty horrendously inefficient, and yet that’s what you have to do if you use the result monad.

3 Likes
6

If we had typed effects (or at least checked exceptions, a restricted form of typed effects) I think it’d be strictly superior to the result monad, too. The problem with monads, in addition to the performance/allocation overhead, is that they compose super badly with all the existing control flow constructs except for function calls. Java’s checked exceptions are not representative of the concept as they never tackled properly the interaction with generics. Done properly, in OCaml, we’d need effects on arrows so that, say, List.map propagates the exception of its functional argument.

7 Likes
7

Yeah, I am very wary of libraries that use exceptions liberally. As it stands, my most frustrating OCaml production bugs have been cases where a library raised an exception that I wasn’t expecting, wasn’t documented, and IMO had no reason to expect, given the calling context.

I do use exceptions on occasion, but almost always for bounded non-local returns (equivalent to labelled break or goto).

2 Likes
8

I don’t know much about how people compose monads (I use the already-composed exception+state+threads+IO monad called “the OCaml compiler”)[1] but I hear there’s this “tagless final something-or-other” that might be relevant. No idea how it works.

But even if monads composed well, and worked for the entire core language, they still don’t work at functor-application and structure-items, right?

[1] One of the arguments made for monads, is that (with the control/threading monad) it allows you to know when-and-where you’ll be time-sliced away, and hence where you have to reason about side-effects. And sure, that’s all fine and dandy in theory. I once worked with a “green threads” system for Python where all context-switches happened with a fixed set of primitive operations: with even a modestly-complex library of code built on-top, you were no longer able to divine where you would or would not be context-switched, and hence had to assume that you could be context-switched anywhere. It was (as I remember putting it) “it feels like a context switch can happen at any newline”. Which is … well, exactly how it feels to use a regular threading system, pretty much. [ok, substitute “any whitespace character”]

1 Like
9

Oh, that sounds like a case of Not_found, an exception that is frustrating because it is so easy to overlook cases where it is thrown as well as quite contextless, since it actually does not specify what wasn’t found. These undocumented exception cases are easy to get wrong because sometimes the author of that code you’re using also wasn’t expecting it, so the surprise is both to you and the library author.

I tend to use exceptions in OCaml in a way inspired by Rust: as panics, to terminate the program when the failure is not recoverable. When I e.g. know that the user hasn’t submitted the required input. Or, as @cemerick mentions, as non-local returns, but then I would guard them.

A similar annoyance to me are by the way Lwt.t promises which, along with being resolved or unresolved can also “fail”, thus forming an unholy alliance of promises and exceptions. It seems like the maintainers of Lwt are aware of this initial design flaw and ship with Lwt_result which handles result nested in Lwt.t (so, exactly as Deferred.Result.t in Async).

7 Likes
10

Cristiano Calcagno has been doing some pretty interesting work on this: reanalyze/EXCEPTION.md at 72712393459d7e132c78e0700abffc5fc4cd09b8 · rescript-association/reanalyze · GitHub

Let me quote the central concept from there:

The exception analysis is designed to keep track statically of the exceptions that might be raised at runtime. It works by issuing warnings and recognizing annotations. Warnings are issued whenever an exception is raised and not immediately caught. Annotations are used to push warnings from he local point where the exception is raised, to the outside context: callers of the current function. Nested functions need to be annotated separately.

1 Like
11

**ding ding ding ding**

One time was my fault directly (via some of my earliest OCaml code where I used find without thinking much about it), the other was exactly the scenario you describe where a borderline edge case parameter to a library function (I think it was an empty string) ended up touching a map with a non-existent key, alas.

I’m certain I’ve groused in irc about Map.S.find being exception-oriented, while the IMO saner semantics are found under the less-natural/longer find_opt. Defaults matter for things like this, so I greatly prefer the foo_exn naming convention for function variants that raise instead of return.

2 Likes
12

François Pessaux worked on exception inference 20 years ago see for example https://hal.inria.fr/inria-00073144. I remember there was an implementation for Ocaml but I have not been able to find quickly its name or a link…

13

This sounds like the main checked-exceptions in Java gave the world. By adding a single exception deep in the stack you had to either handle it immediately or modify the entire call chain. There is a lot of Java code to convert a checked exception into a runtime exception just because it’s too annoying to do right, which means a lot of code handlers errors badly.

14

I wrote two blog posts on my experience using result awhile ago, linked below. Much of it still holds. Many of the pain points others have mentioned do exist, but in my judgement, given the current state of Ocaml, results are strictly better (at the very least at the API boundary, assuming you can convince yourself no exceptions escape it) than exceptions. I also believe that the reasonable error values are necessary. For example, I know some APIs like some variation of ('a, string) result which, IMO, is not a great API as I end up comparing strings and hoping the string value is actually part of the API and not some rando value tossed in there. Double for when meaningful aspects of the error are encoded in the string and I have to decode it to decide what to do.

For my own things I do require that all errors are convertible to a string so I can just show them to the user, this is especially important for development and debugging, IME. This is one of the few places where I do wish we had something like type classes so I could do something like:

foo ()
>>= function
| Ok () -> yadda
| Error err -> show err

YMMV

2 Likes
15

Regarding pretty-printing the exception, why isn’t deriving.show sufficient? IIRC, it supports pretty-printing of extensible variants, and exceptions are such … I remember when I implemented my camlp5/pa_ppx version of deriving.show, I supported extensible variants, and use it to pretty-print exceptions, mimicking the code in either deriving.show, or in deriving.yojson (I forget which, and it’s too late at night or me to go look it up).

1 Like
16

It seems that we had some discussion on this

17

the part in the video at t=20m47s where Prof Thomas tells about the training course after years how to start the system because the operators forgot – that’s hilarious.

1 Like
18

A bit late to the party, but here’s an overview of error handling methods that I did a while ago:

Composable Error Handling in OCaml (keleshev.com)

It compares the following approaches:

  • Exceptions
  • Result type with strings for errors
  • Result type with custom variants for errors
  • Result type with polymorphic variants for errors
9 Likes
19

I have re-read the article and decided to update it to use the recently-introduced Stdlib.Result module and (let*) syntax: https://keleshev.com/composable-error-handling-in-ocaml

5 Likes
20

This tends to be defeated by the implementation of Fun.protect that always saves the backtrace just in case. If you use exceptions for performance you will more and more have to use raise_notrace where it matters.

1 Like