in Coq we would like to modernize our exception handling a bit. Coq’s codebase predates many modern OCaml constructions and thus we have some overlap with existing functionality. In particular, we have:
the Backtrace module, which is used to implement a custom backtrace handling mechanism, and in particular to support re-raise without losing backtrace data. Ideally we would remove this module entirely but there has been reluctance w.r.t. what is the proper way to allow “safe” re-raise.
Exninfo module, which is used to attach other kinds of data to exceptions. I get the feeling that this approach is not in general safe except for debug, non-critical data, but I’m not expert here.
What do you folks think the way forward should be here? Is it possible to have similar functionality with “native” OCaml libs?
Some relevant Coq issues:
What would be your opinion about the exception handling in the style of
Base.Error module? I have found that in general replacing all exceptions with
Base.Or_error.t style returns works exceptionally well, and that using a generic exception like
exception Error of Base.Error.t
when I have to use exceptions, and raising them like
raise (Error (Error.create "invalid index" i [%sexp_of: int]))
works very well, and is very consistent. I presume that the data relevant to debugging, like e.g. backtrace information you’ve mentioned earlier, would be coming in the
Error.t type. Of course, the Coq developers might define their own equivalent of
Error.t, since the dependency even on
Base from JaneStreet may very legitimately be undesirable for this project.
Maybe you will find this one useful:
I look forward to digging into all the packages/tools that people mention; it should be a real eye-opening experience! Recently I found that the “rresult” has some nice exception-trapping and re-raising functionality, and I’ve been switching to it. What’s particularly nice is that it has a nice monadic wrapper, so while
(1) on the one hand I almost NEVER use monads, and kinda sneer at them [so I just trap with the monadic construct, print a message, and re-raise]
(2) on the other hand, WHEN I want to trap exceptions and pile 'em up until I’m ready to deal with 'em (e.g., typecheck list of expressions, and only at the end deal with any errors that were found), rresult is conveniently precisely what I want.
But I’m a complete foreigner to using libraries for this, so I’m sure there’s something better, and I look forward to learning what it is!
Recently, some syntactic support for monads was added to OCaml.
“Binding operators (
and* , etc). They can be used to streamline monadic code.” Cf. https://ocaml.org/releases/4.08.0.html
I wonder if this will influence the style of OCaml programs, over the long run.
By the way, if there is a tutorial or some nice doc somewhere on those new
binding operators, I’ll happily read it.
PS: I found some material on the new binding operators https://jobjo.github.io/2019/04/24/ocaml-has-some-new-shiny-syntax.html and http://caml.inria.fr/pub/docs/manual-ocaml/manual046.html