Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Extend try with "success" handling #6318

Closed
vicuna opened this issue Feb 4, 2014 · 30 comments
Closed

Extend try with "success" handling #6318

vicuna opened this issue Feb 4, 2014 · 30 comments
Assignees
Milestone

Comments

@vicuna
Copy link

vicuna commented Feb 4, 2014

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
Copy link
Author

vicuna commented Feb 4, 2014

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
Copy link
Author

vicuna commented Feb 4, 2014

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
Copy link
Author

vicuna commented Feb 6, 2014

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
Copy link
Author

vicuna commented Feb 6, 2014

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
Copy link
Author

vicuna commented Feb 6, 2014

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
Copy link
Author

vicuna commented Feb 6, 2014

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
Copy link
Author

vicuna commented Feb 6, 2014

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
Copy link
Author

vicuna commented Feb 7, 2014

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
Copy link
Author

vicuna commented Feb 7, 2014

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
Copy link
Author

vicuna commented Feb 7, 2014

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
Copy link
Author

vicuna commented Feb 7, 2014

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
Copy link
Author

vicuna commented Feb 7, 2014

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
Copy link
Author

vicuna commented Feb 10, 2014

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
Copy link
Author

vicuna commented Feb 11, 2014

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
Copy link
Author

vicuna commented Feb 11, 2014

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).

@vicuna
Copy link
Author

vicuna commented Feb 11, 2014

Comment author: @gasche

I feel that the patch lacks a testsuite exercising the feature. I just
considered trying to tweak a few things in the new patch, but the lack
of correctness feedback is discouraging.

Some remarks, then:

  • I regret that you partition clauses at the parsing stage, because
    that means -dsource, and -dtypedtree even more, will be unable to
    print the code in a style isomorphic to what the user wrote. I would
    keep the clause list unsplit in the parsetree, and even in the
    typedtree if it doesn't obfuscate code too much (I don't see why
    it would); in fact it could even simplify the patch

  • we want to handle the case where there are exception clauses, and
    the scrutinee is a tuple; my implementation idea was to implement
    the binding+staticcatch wrapping logic as a combinator taking a code
    generation continuation

@vicuna
Copy link
Author

vicuna commented Feb 11, 2014

Comment author: bmillwood

I don't really see the dangling situation worsened very much, since you pretty much already need to enclose nested matches in begin...end.

But yes, "the patch is already written" is a major argument in favour of the other syntax :) I don't object to it particularly.

@vicuna
Copy link
Author

vicuna commented Feb 11, 2014

Comment author: @alainfrisch

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.

Yes, of course, the concrete syntax would remain backward compatible, but the changes to the Parsetree would be more invasive, thus potentially requiring more work on external tools which operate on this representation.

Generally speaking, extending "algebraic" categories (i.e. sum types) in the Parsetree plays nicer with external tools than extending record types or tuples.

@vicuna
Copy link
Author

vicuna commented Apr 2, 2014

Comment author: @alainfrisch

It would be great to have this feature in 4.02, whose feature freeze date might come soon (in one month or so, it seems).

Any volunteer to apply the suggested changes? Namely:

  • Writing a testsuite.

  • Minimizing impact on the parsetree and doing the split between the two kinds of clauses during type-checking, by adding a case to the algebra of patterns. (So that further extensions, allowing e.g. to mix value and exception patterns, or supporting exception patterns under lazy, won't require any change to the parsetree.)

@vicuna
Copy link
Author

vicuna commented Apr 2, 2014

Comment author: @yallop

Thanks for the prompt. I have a testsuite, which I'll add to the patch shortly.

With regard to the changes to the parsetree, I agree that the current implementation is less than ideal. The two arguments against it that I find most convincing are:

(1) (Alain's) that it will require further significant changes to support things like 'lazy exception PAT'

(2) (Gabriel's) that it breaks pretty printing, since it discards the original structure of the code

I'm certainly happy to change the representation to address these. The two proposals, both of which would fix these problems, are

(a) to extend the pattern algebra with 'exception PAT'. This has the advantage of minimising the initial impact on external tools. The potential drawback is that it makes the representation less 'tight': since 'exception' is invalid in most pattern contexts, we may end up checking for exception patterns and signalling errors all over the place, both in the compiler and eventually in external tools as well.

(b) to distinguishing 'value' patterns from 'effect' or 'computation' patterns. This has the advantage of representing exactly where 'exception PAT' can occur in the AST. The potential drawback is that it adds duplication: we'd need to support things like 'or' patterns for both value and effect patterns.

It might be worth implementing both approaches to determine how much of a nuisance the potential drawbacks actually turn out to be.

The other change that's needed is support for the the special handling of tuple matches, as Gabriel points out.

@vicuna
Copy link
Author

vicuna commented Apr 3, 2014

Comment author: @alainfrisch

Thanks Jeremy.

My intuition is that (a) is better, because it avoids the need to introduce new syntactic categories (which requires to extend e.g. the signature of ast mapper objects and adds complexity to the grammar definition). Moreover, (b) would make it harder to give nice error messages (or you would need to extend the parser with rules to detect a syntactically valid pattern, but used in a wrong context), while it would come naturally in the type-checker (to make pattern matching exhaustive).

@vicuna
Copy link
Author

vicuna commented Apr 5, 2014

Comment author: @gasche

A remark on pretty-printing: I've since found out that many other parts of the parsetree are treated as lossy desugaring and won't pretty-print in the way they were first written (for example "fun x -> fun y -> ..."). I don't think we should require new features to respect a roundtrip constraint that isn't currently respected, and for which there are no strong incentives right now -- nobody uses -dsource, basically, and it's often useless as it removes comments and whitespace.

@vicuna
Copy link
Author

vicuna commented Apr 7, 2014

Comment author: @alainfrisch

I agree with Gabriel, but I still see a lot of values of minimizing the impact on the Parsetree definition. It's better if all syntactic tools which need to inspect pattern matchings don't need to deal with "exception" cases specifically, and they won't have to be adapted if/when "exception" is allowed in more contexts.

@vicuna
Copy link
Author

vicuna commented Apr 24, 2014

Comment author: @yallop

I've updated the patch with the testsuite. The full diff is here:

ocamllabs/ocaml@3775a10...handler-syntax

and the testsuite is here:

ocamllabs@cbcccb52

I've extended the special-casing of tuple matches to the new syntax, so that the following sort of thing doesn't allocate:

match (a, b) with
  (x, y) -> e1
| exception E -> e2

I've partly implemented the proposal for extended the pattern algebra rather than the Pexp_match constructor, but not yet included it in the patch. I'm not sure how to best implement (e.g.) Typecore.type_cases, which expects to a single set of cases with a single argument type, without doing more violence to the current code than I'm comfortable with. Suggestions welcomed.

The patch is also rebased against trunk.

@vicuna
Copy link
Author

vicuna commented Apr 25, 2014

Comment author: @alainfrisch

Thanks Jeremy!

In Typecore.type_approx, you seem to use the first exn-case to get the approximation. Shouldn't you use the first val-case instead?

I'm not sure how to best implement (e.g.) Typecore.type_cases

I'd simply do the same as what Parser.partition_handler_cases does, i.e. define a function which splits the list of cases stored in the parsetree into two lists (and removes the "exception" wrappers). Something like:

let split_cases vc ec = function
| [] -> List.rev vc, List.rev ec
| {pc_lhs = {ppat_desc=Ppat_exception p}} as c :: rest ->
split_cases vc ({c with pc_lhs = p} :: ec) rest
| c :: rest ->
split_cases (c :: vc) ec rest

@vicuna
Copy link
Author

vicuna commented Apr 25, 2014

Comment author: @yallop

you seem to use the first exn-case to get the approximation

Good point. Of course, the types of val and exn cases will be the same, but the list of exn cases may be empty, so it's better to use the val cases for type approximation.

I'd simply do the same as what Parser.partition_handler_cases does

Indeed, it's straightforward to split the cases into two lists and type those separately. The awkward part comes when they need to be put back together afterwards. I can see three possibilities:

(1) Keep track of the original positions of the cases during partitioning, then use the positions to reassemble the combined list after typing. This is the best way to maintain the original structure of the AST, but makes the code in the type checker rather awkward.

(2) Leave the typed tree as it currently is in the patch (i.e. with separate fields for val and exn cases).

(3) Change the typed tree to use a single list of cases, but make no attempt to recover the original case ordering.

Do you have a preference?

@vicuna
Copy link
Author

vicuna commented Apr 25, 2014

Comment author: @alainfrisch

I don't have a strong preference. While keeping the Parsetree simple and stable is important (because of -ppx in particular), I think we have more freedom for the Typedtree, so I think the simplest solution (probably 2) would be ok for now. We can always refine that later, it's unlikely to break many tools.

@vicuna
Copy link
Author

vicuna commented Apr 25, 2014

Comment author: @yallop

Leaving the Typedtree as it is makes things much easier. Here's the latest patch, which extends the pattern algebra rather than Pexp_match:

ocamllabs/ocaml@2633ff7...handler-syntax

@vicuna
Copy link
Author

vicuna commented May 5, 2014

Comment author: @alainfrisch

Ok, I've integrated the patch (after restoring the check that the list of value cases is non-empty). Thanks a lot, this is a much welcome addition to the language!

@vicuna
Copy link
Author

vicuna commented May 5, 2014

Comment author: @alainfrisch

The manual and ppx_tools have been adapted as well.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

2 participants