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).
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
resulttype 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 that neatly defines it (and goes into some detail of how to go about achieving it); from the accompanying lecture notes:
…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.
: Making Software ‘Correct by Construction’ https://www.gresham.ac.uk/lectures-and-events/making-software-correct-by-construction