Could this be extended to handle exception branches as well? Originally asked in #1947 (comment) and responded to by @yallop in #1947 (comment)

@hcarty, we'll probably have to disallow exception under or patterns such as

match+ expr with
| None | exception Not_found -> case 1
| Some _ -> case2

@hhugo: the first scheme I gave handles exceptions under or patterns. Your example

match+ expr with
| None | exception Not_found -> case1
| Some _ -> case2

is translated to

(match+)
  (function Ok None | Error Not_found -> case1 | Ok Some _ -> case2)
  (match expr with x -> Ok x | exception e -> Error e)

The second scheme can also handle a few cases of exceptions under or patterns, but it needs to either duplicate the continuation expressions (i.e. case1, case2), or pull them out as let bindings, which may not work if GADT patterns are involved.

One additional issue with handling exceptions is exhaustiveness: since exception cases (like exception Not_found) are allowed to be inexhaustive, whereas patterns for exception value (like Not_found) are checked for exhaustiveness, a bit of extra care is needed to avoid spurious warnings. Perhaps something like adding a catch-all case with warning 11 disabled could be made to work.

I like this proposal. I have a ppx extension (not published) that performs the same translation, because I quite often write code like this in MetaOCaml programs

match_ x @@ function
| Some false -> .< e1 >.
| Some true -> .< e2 >.
| None -> .< e3 >.

and prefer to write something closer to the standard match syntax, without explicit use of higher-order functions.

Comments:

1. Like @hcarty, I'd like to see support for exception patterns, perhaps based on the result-based scheme I sketched above.

2. I'd prefer to see the order of arguments reversed, so that the continuation function comes last. Reasons:
   (a) the order matches the standard order of monadic bind, so it's more harmonious with existing code
   (b) at present, disambiguation appears to work better with the function-last order. Given the following definitions

   module M = struct type t = T end
   module N = struct type t = T end
   open M
   open N
   let match1 x f = f x and match2 f x = f x
   let mt = M.T and nt = N.T

   this code is accepted:

   match1 mt (function T -> ())

   but this function is rejected:

   match2 (function T -> ()) mt

3. It's interesting to see to what extent the standard syntax can be replaced using the extension. Here's one case where I don't think replacement works seamlessly at present:

type (_,_) eql = Refl : ('a,'a) eql
let cast : type a b. (a,b) eql -> a -> b =
  fun e x -> match e with Refl -> x

In the above code, it doesn't seem possible to rewrite the body of cast using a match+ operator without adding additional type annotations.

Do you think this will make it into the next release? It would be very helpful to have the let and match versions land at the same time to avoid fragmenting code between native syntax support for let and ppxs for match.

If they won't both land for 4.08.0, is it worth delaying both to a later release so they can be adopted by the community together?

@lpw25 For the moment, we have merged let operators but not this one. Are you satisfied with this state?

Yes, I think that is fine for now.

At Issuu, we use ppx_let extensively for let%bind, match%bind, et al. The only thing preventing us from migrating to the new monadic operators is the lack of support for match. Are there still open questions regarding this PR, or can we expect this feature to be available sometime in the near future? 🙂

Coming to this PR after a while:

• It would be nice to see this issue move forward.
• If we do want to handle exception clauses in match operators, my favorite proposal is @yallop's using a matching on ('a, exn) result -- making sure to not raise an exhaustivity warning for the Error parts.
• But I am still not convinced that it is a good design to impose the conceptual cost of result for all match operators. I can see many different monads where handling exceptions in this way does not make sense, and as a library author I would rather work with the simpler type and prevent my users from trying to use exception clauses.
• Ideally there would be a clear static scheme do decide which translation to use (exception-handling or not), so that library authors can decide to support one or the other. But I can't think of such a scheme right now, except possibly an attribute at declaration-site, and it seems relatively ugly/ad-hoc. Any suggestions?

An option would be to elaborate differently depending on whether there is a exception pattern or not. We'd need an extra class of identifiers (exception match<op-chars>). The above example would be

(exception match+)
  (match expr with m -> Ok m | exception exn -> Error exn)
  (function Ok None | Error Not_found -> case1 | Ok Some _ -> case2 | Error exn -> raise exn)

and without the exception case

(match+)
  expr
  (function None -> case1 | Some _ -> case2)

Exceptionless monads would omit (exception match+), while exceptionful monads could in principal use it to implement

let (match+) m f =
  (exception match+)
    (Ok m)
    (function Ok x -> f x | Error exn -> raise exn)

I like the idea, thanks! What about (match+ with exception) as the operator name? This is the name ("match with exception") I used to describe this feature.

This being said, there is something that bugs me about the choice of elaboration on the scrutinee (match expr with x -> Ok x | exception e -> Error e). It seems to assume that the "error" cases in the monad come from the OCaml expression actually raising an exception. But in general this is not what happens, "errors" are (pure) monadic operators that get interpreted as failures. For example in the option monad I would maybe expect to be able to write

return : 'a -> 'a option
val fail : 'a option
val (match+ with exception): 'a option -> (('a, unit) result -> 'b) -> 'b
let (match+ with exception) m f =
  match f with
  | Some v -> f (Ok v)
  | None -> f (Error ())

(* example usage *)
val map : ('a -> 'b) -> 'a option -> 'b option
let map f m = match+ m with
  | x -> return (f x)
  | exception () -> fail

Note that here the translation I expect is that the branches are made result-expecting, but the scrutinee itself is passed unchanged.

Does that make sense? (@yallop?)

My plan was to allow binding things like (exception*) and then translate:

match* e1 with
| p1 ->e2
| exception* p2 -> e3

into:

(match*) ((exception*) e1)
  (function
  | Ok p1 -> e2 
  | Error p2 -> e3)

Intended to be used with functions of type:

val (exception*) : 'a t -> ('a, foo) result t

This fits in well with how (and*) works. Although, it doesn't really work for multiple different (exception) operators in the same match.

Possibly we should be thinking in more terms general terms. (and) operators are based on applicative functors, perhaps something like selective functors would give a good foundation for (exception) operators.

Although, it doesn't really work for multiple different (exception) operators in the same match.

Could you give an example that doesn't work with this scheme?

I just meant that my proposal suggests that you might be able to write something like:

match* e1 with
| p1 -> e2
| exception++ p2 -> e3
| exception-- p3 -> e4

with two different exception operators, but I don't think there is an obvious translation for such code.

A way to translate different exception operators would be

(match*)
  ((exception--) ((exception++) e1))
  (function
   | Ok (Ok p1) -> e2
   | Ok (Error p2) -> e3
   | Error p3 -> e4)

The order of application can be takes as the order of occurrence, since the matches will be disjoint and therefore can be ordered by the user as needed, but it's probably better that the implementation ensure they commute.

@gasche I agree (match* with exception) is more instructive, though now I think I favour the decoupling into (exception*) operator(s). I also was considering whether catching exceptions are the right approach. If we wish to leave control over that to the implementation, we can instead rewrite the scrutinee as a thunk.

Is there a compelling reason to support separate operators for each exception pattern when we don't have separate operators for each value pattern?

The fact that we have a keyword for exception patterns but not value patterns is more an accident of history than a fundamental property of matching. (We almost ended up doing things the other way around.)

As a user, I would expect an | exception e -> ... branch to catch and give me an actual exception (exn), not arbitrary values unwrapped from results. If I am encoding possible errors as results, I can already match on Ok|Error _ directly. Matching it in an exception _ branch imho does not increase expressivity but does introduce a new meaning (exception e can catch any value, not just an exception) to a syntax which before had only one meaning.

Also, will this interact with effect handler syntax?

Is there a compelling reason to support separate operators for each exception pattern when we don't have separate operators for each value pattern?

Not really. I was more pointing out that my proposed scheme kind of implies that you can write such a thing. If we do use my scheme then I'd prefer that we insist that all exception operators in a match are the same, and just error otherwise.

I would expect an | exception e -> ... branch to catch and give me an actual exception

This is a match applied to a monadic computation, not a computation in OCaml's implicit monad. The "exceptions" that it catches should be operations of the monad used in the computation. A number of monads have an operation that is isomorphic to catching an exception, not all of them use the exn type for these exceptions. The use of result is just a convenient mechanism for exposing the exception-handling operations -- it would not be visible to users of the monad/syntax.

will this interact with effect handler syntax?

It would be a bit difficult to make the typed effect syntax available for use with monadic computations, and I don't know of any monads which provide effect handling operations. (Possibly something from the "scoped effects" line of work would.) So I don't think we'll extend this support to work with effect syntax.

What happens when the exception matching is incomplete, like it normally is? If the elaborated pattern matching raises a regular exception, (match*) could not (in an obvious way) tell if it's a regular or monadic case. So maybe (exception*) needs to be paired with a function to return en error back into the monad?

val (exception*) : 'a t -> ('a, error) result t
val (raise*) : error -> 'a t

And should an undecorated exception only catch a regular exceptions? That is:

match* expr with
| v0 -> Some v0
| exception* Not_found -> None
| exception Failure _ -> None

elaborates to

match expr with
| exception Failure _ -> None
| m ->
  (match*)
    ((exception*) m)
    (function
     | Ok v0 -> Some v0
     | Error Not_found -> None
     | Error err -> (raise*) err)

Examples

I wish we would discuss with more concrete examples of algebraic structures using these operators, with implementations of the operators and use-cases for them. So far we have exactly one example (#1955 (comment)). using 'a option. It's a bit short for a design discussion.

Types

I have the impression that (match+ with exception) and (exception+) are equi-expressible. In the case of applicative functors (for example):

val (let+) : 'a t -> ('a -> 'b) -> 'b t
val (match+ with exception): 'a t -> (('a, foo) result -> 'b) -> 'b t
val (exception+) : 'a t -> ('a, 'foo) result t

let (expection+) v = (match+ with exception) v Fun.id
let (match+ with exception) v f = (let+) ((exception+) v) f

(exception+) has a a simpler type, which is a strong argument in favor.

On the other hand, it raises pesky syntactic questions -- one nice thing with (match+ with exception) is that the exception keyword does not have to be customized, and there are no questions about allowing several different customizations, etc. One could decide that the user syntax is to write match<op> ... with ... | exception p -> ..., and then lookup (exception<op>) to avoid this issue.

(raise*)

I find @paurkedal proposal to have a re-raising operation interesting, but note that the question also arise for value matches: some monads have a natural notion of failure that is better than raising a Match_failure exception, do we want to allow something like (match+ failure) in this case as well?

@paurkedal:

And should an undecorated exception only catch a regular exceptions? That is:

match* expr with
| v0 -> Some v0
| exception* Not_found -> None
| exception Failure _ -> None

elaborates to

match expr with
| exception Failure _ -> None
| m ->
  (match*)
    ((exception*) m)
    (function
     | Ok v0 -> Some v0
     | Error Not_found -> None
     | Error err -> (raise*) err)

I don't like this proposal. I don't think the notion of "monad whose computations can also raise native exceptions" is sensible. What we have in certain libraries is an interplay of two sorts of effects, those captured by the monad (possibly with some notion of failure) and "native" failures (exceptions). If you want to play at the two levels at once, you have to deal with two sets of operators (just like you mix code from two different monads); this is conceptually more regular than trying to have a single operator play at the two levels.

Note that the proposed desugaring is also not expressive enough to cover all of the try%lwt behavior, which will reraise uncaught exceptions using Lwt.fail.

I don't think the notion of "monad whose computations can also raise native exceptions" is sensible.

The point was, on the contrary, to decouple monadic failure and regular exceptions. The exception clause in the example acts like on a regular match. So this was more a matter of giving sensible (but uninteresting) semantics to the exception case, but:

Note that the proposed desugaring is also not expressive enough to cover all of the try%lwt behavior, which will reraise uncaught exceptions using Lwt.fail.

If I understand correctly, I agree this will not cover the Lwt approach of automatically converting regular exceptions to monadic failure. I suspect we don't want to do this directly in the elaborated code, since it would restrict exception* patterns to the exn type. We could instead turn the scrutinee into a thunk to leave the decision to (match*) or (exception*).

Out of curiosity, what is the status of this PR?

I'd like to finish it off, including support for either (exception*) or (match* with exception), but we don't use binding operators at Jane Street -- preferring to stick with ppx_let -- so I'm not likely to get around to it. Perhaps someone else would like to push it forwards.

15 months later, does someone else wishes to push this idea forwards? Personally I'm not a big fan of the proposed feature, but could still be convinced.

Let's just close it. Someone can always pick it up again later.