Extend try with "success" handling

[vicuna]

Original bug ID: 6318
Reporter: @yallop
Assigned to: @alainfrisch
Status: closed (set by @xavierleroy on 2015-12-11T18:26:59Z)
Resolution: fixed
Priority: normal
Severity: feature
Target version: 4.02.0+dev
Fixed in version: 4.02.0+dev
Category: ~DO NOT USE (was: OCaml general)
Tags: patch
Related to: #6422 #6423
Monitored by: @gasche @diml @ygrek bobot @jmeber @hcarty yminsky @mmottl

Bug description

I'd like to propose extending try with clauses that match the value of the body in the case where no exception is raised:

try expr
with pattern_1 -> expr_1
   | ...
   | pattern_n -> expr_n
   | val pattern_1' -> expr_1'
   | ...
   | val pattern_n' -> expr_n'

Adding a place to specify what should happen only in the "success" case has two benefits: it makes some code clearer, and it makes it easier to write tail recursive code, since expr_1'...expr_n' are in tail position.

I've posted a more detailed proposal here, with an implementation and some history:

http://ocamllabs.github.io/compiler-hacking/2014/02/04/handler-case.html

[vicuna]

Comment author: @alainfrisch

in this case the value of expr is matched against pattern_1' ... pattern_n' to select the expression to evaluate to produce the result value

The feature is great, but I really dislike the choice of the "try...with" syntax. What happens if none of these pattern match the value of expr? There are two possibilities:

i) The value of expr itself is returned: this is coherent with the current behavior of try...with, but it forces the type of the expr to be the same as the entire expression, and when the "val" clauses are exhaustive, there is no reason to do so.

ii) As soon as there is one "val" branch, the value of expr must be matched by one of them. This is very "discontinuous": the presence of a single branch changes the fact that the value of expr can be or not the value for the entire expression (which affects how the construction is type-checked). And that behavior would be so different from the current try...with (where the result is either the one from 'expr' or from one of the branches) that sharing the syntax would not be wise.

The most useful behavior is ii) (because one can add explicitly a catch all case "val x -> x" to retrieve i)).

The alternative syntax based on 'match...with' seems much better to me. And this is really what the new construction is: it matches the (exceptional or not) result of 'expr' and use it to pick the continuous.

[vicuna]

Comment author: @mmottl

@Frisch: the lack of "continuity" as you would call it is a good point. Adding a "val" pattern would shift the type of the whole expression from the "try" expression to the right hand side of patterns, which is awkward.

I'd also dislike solutions that keep value and exception patterns apart. This would make it impossible to use the same right hand side for exception and value patterns as in:

match expr with
| exception (Foo n) | Some n -> ... use n ...
| exception _ | None -> ...

It seems the "match...with"-syntax by itself works best so far in any use case. I think there is no need to rush for a "try"-solution if it seems awkward. Chances are that people would already be happy enough with the "match/exception"-solution.

[vicuna]

Comment author: @alainfrisch

I don't think Jeremy gave the pointer to the branch, so here it is, for those who might want to review the patch:

https://github.com/ocamllabs/ocaml/commits/handler-syntax

[vicuna]

Comment author: @alainfrisch

The patch shows clearly that having a non-empty set of "val" clauses in the try...with construction changes radically its type-checking rule (typecore.ml). This is a sign that the same syntactic form would be used for two different things, which is rather bad.

The corresponding change for the extended match...with is more regular. Actually, I think the two cases (with or without "exception" clauses) in typecore could and should be merged. Can you explain why you dropped begin_def() and end_def() from the case with "exception" clauses?

Concerning the implementation:

• one should of course draw fresh static_exception_ids instead of always using (-1).

• you observed that some optimization in simplif.ml has to be disabled for static exceptions (the optimization only applies when the staticraise is necessarily in tail position, which used to be the case when generated by the pattern-matching compiler). The technique I used in my static exception branch was to use negative identifiers for static_exceptions which should not be subject to this optimization (i.e. those introduced by the new feature). See: http://caml.inria.fr/cgi-bin/viewvc.cgi/ocaml/branches/static_exceptions/bytecomp/simplif.ml?r1=13216&r2=13217

[vicuna]

Comment author: @alainfrisch

Regarding Markus' comment about allowing to mix val and exception clauses: I agree it would be a nice addition, and it doesn't seem too difficult to implement. The idea would be to introduce one extra static_handler for each case (and let simplif.ml simplifies the typical case where it is used only once; or otherwise do it only for cases which mix val and exception patterns). (Well, perhaps guarded cases would be more difficult to support without duplicating the code the guard...)

---

On a related note, I'd be in favor of adding the "exception PAT" as a new construction in the algebra of patterns instead of letting the parser split "val" and "exception" clauses. The type-checker would normally fail on this new form of pattern, and the type-checking rule for the match...with would apply a special treatment to "split" a pattern by recognize the new form at the toplevel or immediately under (nested) or-patterns.

This would minimize the impact on the Parsetree and make the grammar more regular (no need to introduce new notion of "cases"), simplify the parser, and probably allow for better error messages when the user writes e.g.

| (exception ...) as foo -> ...

[vicuna]

Comment author: @garrigue

Just my grain of salt.

I kind of agree with Alain: this is an extension of match, and would better be implemented as such.
Considering the syntax, this is true that one wants the handling part to be very visible, but is it not the case already if we use the "exception" keyword?
Somehow "try" may end up deprecated some day, but removing keywords should be seen as a good thing!

For combining values and exceptions in the same or-pattern, I would be careful.
Depending on how it is compiled, combining the two together may make it more complicated.
On the other hand, if this can be made efficient I agree that it is something you may want.

[vicuna]

Comment author: @alainfrisch

Another argument in favor of extending the syntax of patterns with an "exception PAT" form would be to support things such as:

match ... with
| ...
| ... lazy (exception Not_found) ... -> ...
| ...

(I'm not proposing to support this right now, because it would complicate the compilation quite a bit.)

[vicuna]

Comment author: @alainfrisch

Does the following sound reasonable to everybody?

• Discard the extended try...with syntax and keep only match...with with "exception" clauses.

• Extend the syntactic algebra of patterns with "exception PAT".

• For now, support only toplevel occurrences of this new form of patterns in match...with clauses (in particular, do not try to support them under or patterns).

(Support for "exception PAT" under or-patterns (and maybe under lazy patterns) can then come later without changing the syntax.)

[vicuna]

Comment author: @gasche

Yes, but I'm disturbed by point 2 (consider (exception p) a meaningful pattern in the general case). I agree the lazy example makes sense, but I think it rather means we should distinguish two syntactic classes, "value patterns" and "effect patterns", and that (lazy p) should in fact take an effect sub-pattern.

I think it is obvious to most people here but I would also like to clarify that:
match e with
| p1 -> ...
| p2 -> ..
| exception p1 -> ...
| exception p2 -> ...

can be understood as syntactic sugar for the internal syntax
match e with
| val p1 -> ...
| val p2 -> ..
| exception p1 -> ...
| exception p2 -> ...

In particular, (match e with _ -> e') gives an universal value pattern, and not an universal effect pattern, and does not capture exceptions.

[vicuna]

Comment author: @gasche

Remark that Alain suggests to support only match..with, because the static semantic of try..with is more awkward, whereas they have a perfectly symmetric dynamic semantics.

The fundamental reason for the awkwardness is that exceptions are not statically typed in ML. If we were to have exception typings, we would see that extending match..with changes its exception typing in a discontinuous way, just like what Alain doesn't like about the extended try..with.

I still like the idea of having both, but agreeing on extending match..with is a good compromise. In particular, there is not much hope of being able to factorize try..with and its extension, as they handle "expected type" (the small amount of bidirectional type-checking we have for GADTs) differently than the non-extended version. On the contrary, typing rules for extended match..with can be merged with the existing one: the bidirectional information lost is the exception typing, which we do not track anyway.

[vicuna]

Comment author: @alainfrisch

Yes, but I'm disturbed by point 2 (consider (exception p) a meaningful pattern
in the general case). I agree the lazy example makes sense, but I think it
rather means we should distinguish two syntactic classes, "value patterns" and
"effect patterns", and that (lazy p) should in fact take an effect sub-pattern.

Do you suggest two distinguish the two categories in the Parsetree (with a lot of duplicates, e.g. the | can be used in both kinds)?

My proposal attempts to minimize the impact on the syntactic aspects, while pushing the distinction between effect and value patterns to the type-checker.

[vicuna]

Comment author: @gasche

Do you suggest two distinguish the two categories in the Parsetree
(with a lot of duplicates, e.g. the | can be used in both kinds)?

I don't have a strong opinion. I think they should be distinguished in the manual, for example. I'm also not sure that would actually incur duplication. (p | p) is a valid value pattern, but there is not much incentives to allow it on effect patterns (if we don't want to allow (val p | exception p), all other cases can be expressed by lifting eg. (val p | val p') to (val (p | p')), and the external | between clauses would only take effect patterns (with some extra annotation to be able to pretty-print the simple (p) as (p) instead of (val p)).

[vicuna]

Comment author: @yallop

Thanks for the comments and code review. I've made a new version of the patch available here:

yallop/ocaml@trunk...handler-syntax

The changes are:

• Only the extended match syntax is supported. The extended try syntax is no longer supported.

• Translcore.transl_exp0 now uses a fresh id each time instead of always using -1. (Thanks, Alain.)

• I fixed a bug in translcore where match totality information was not propagated.

• I reused the checks from Alain's static exception branch to disable optimizations for static raises not in tail position in Simplif.simplify_exits.

• I merged the two cases in the type checker for unextended and extended match. (Thanks, Alain.) The omission of begin_def/end_def was an oversight; the code was based on the code for Pexp_try (which doesn't use begin_def/end_def) rather than Pexp_match (which does).

• The previous implementation supported match expressions with only exception-matching clauses:

  match v with exception E -> e   ~>   v
  

  Going by the discussion so far this seems unlikely to be a popular feature, so I removed it. The type checker now catches such expressions and reports an error:

  # match v with exception E -> e;;
  Characters 0-29:
    match v with exception E -> e;;
    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  Error: None of the patterns in this 'match' expression match values.
  

I haven't yet changed the algebra of patterns to include 'exception PAT', since there doesn't seem to be consensus on this point yet. One possible drawback of such a change is that 'exception PAT', unlike existing pattern forms, doesn't make sense in most pattern contexts; for example, it can't be used in 'function' or 'let' bindings, both of which involve value patterns rather than effect patterns (to use Gabriel's terminology). I like the idea of allowing 'exception PAT' inside lazy and 'or' patterns, though; this should be possible in future regardless of whether we change the match syntax or the pattern syntax now.

[vicuna]

Comment author: bmillwood

Hi, following the discussion on the mailing list I was asked to present my view here:

I agree that 'exception PAT' should not be a pattern. In almost all pattern contexts it doesn't make sense, so if it really feels important to support 'lazy (exception PAT)' then I suggest we do so by allowing 'lazy' to take more than a pattern. (I do wonder what our semantics are for an exception-catching match statement, that also throws an exception while matching a lazy value. Do we catch it?)

With that in mind, I suggest that branches that match values are really quite different and separate from branches that match exceptions, e.g. in that

match v with | x -> ... | exception e -> ...

is always the same as

match v with | exception e -> ... | x -> ...

and in the behaviour of wildcard matches.

So, on the mailing list I proposed a syntax which more clearly distinguished the two kinds of patterns, and as a side effect made the meaning of wildcard patterns completely unambiguous. Something like:

match v with
| V1 -> ...
| V2 -> ...
with exception
| Ex1 -> ...
| Ex2 -> ...

I hadn't at the time considered the benefit of clauses like

match v with | None | exception Not_found -> ... | Some x -> ...

and I don't have a good answer for that in my syntax. But I wonder if that's so common a use case, and might be considered worth sacrificing for the greater clarity of my approach.

If we were feeling extra keen, we might have a look around at existing code to see whether it would benefit from this new form and if so in what way. For example, code that uses Core and contains 'match Option.try_with' (or Result or Or_error instead of Option) might be worth looking at.

[vicuna]

Comment author: @gasche

A problem with that syntax is that it worsens the (already-existing) "dangling with" issues:

match v1 with
| p1 -> ...
| p2 -> match v2 with
| p3 -> ...
| p4 -> ...
with exception
| p5 -> ...
| p6 -> ...

Otherwise I feel both proposals are reasonable, and would be a net improvement over the statu quo (having none). Given that there already is a patch for the not-split syntax, I would tend to favor it (it's better if we can converge to a single consensual proposal).