Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006318OCamlOCaml generalpublic2014-02-04 19:032014-04-07 17:36
Reporteryallop 
Assigned Tofrisch 
PrioritynormalSeverityfeatureReproducibilityN/A
StatusassignedResolutionopen 
PlatformOSOS Version
Product Version 
Target Version4.02.0+devFixed in Version 
Summary0006318: Extend try with "success" handling
DescriptionI'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 [^]
Tagspatch
Attached Files

- Relationships

-  Notes
(0010880)
frisch (developer)
2014-02-04 21:37

> 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.
(0010881)
mottl (reporter)
2014-02-04 23:13

@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.
(0010895)
frisch (developer)
2014-02-06 10:34

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 [^]
(0010896)
frisch (developer)
2014-02-06 11:01

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 [^]
(0010897)
frisch (developer)
2014-02-06 11:19

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 -> ...
(0010898)
garrigue (manager)
2014-02-06 11:57

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.
(0010900)
frisch (developer)
2014-02-06 13:59

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.)
(0010906)
frisch (developer)
2014-02-07 10:32

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.)
(0010907)
gasche (developer)
2014-02-07 10:48

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.
(0010908)
gasche (developer)
2014-02-07 10:54

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.
(0010909)
frisch (developer)
2014-02-07 11:28

> 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.
(0010910)
gasche (developer)
2014-02-07 13:25

> 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)).
(0010917)
yallop (developer)
2014-02-10 20:08

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

   https://github.com/yallop/ocaml/compare/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.
(0010918)
bmillwood (reporter)
2014-02-11 14:04

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.
(0010919)
gasche (developer)
2014-02-11 14:15

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).
(0010920)
gasche (developer)
2014-02-11 14:30

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
(0010921)
bmillwood (reporter)
2014-02-11 15:32

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.
(0010922)
frisch (developer)
2014-02-11 15:38

> 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.
(0011184)
frisch (developer)
2014-04-02 23:05

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.)
(0011189)
yallop (developer)
2014-04-03 00:52

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.
(0011206)
frisch (developer)
2014-04-03 12:03

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).
(0011231)
gasche (developer)
2014-04-05 11:17

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.
(0011241)
frisch (developer)
2014-04-07 17:36

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.

- Issue History
Date Modified Username Field Change
2014-02-04 19:03 yallop New Issue
2014-02-04 21:37 frisch Note Added: 0010880
2014-02-04 23:13 mottl Note Added: 0010881
2014-02-06 10:34 frisch Note Added: 0010895
2014-02-06 11:01 frisch Note Added: 0010896
2014-02-06 11:19 frisch Note Added: 0010897
2014-02-06 11:25 frisch Assigned To => frisch
2014-02-06 11:25 frisch Status new => assigned
2014-02-06 11:25 frisch Target Version => 4.02.0+dev
2014-02-06 11:57 garrigue Note Added: 0010898
2014-02-06 13:59 frisch Note Added: 0010900
2014-02-07 10:32 frisch Note Added: 0010906
2014-02-07 10:48 gasche Note Added: 0010907
2014-02-07 10:54 gasche Note Added: 0010908
2014-02-07 11:28 frisch Note Added: 0010909
2014-02-07 13:25 gasche Note Added: 0010910
2014-02-10 20:08 yallop Note Added: 0010917
2014-02-11 14:04 bmillwood Note Added: 0010918
2014-02-11 14:15 gasche Note Added: 0010919
2014-02-11 14:30 gasche Note Added: 0010920
2014-02-11 15:32 bmillwood Note Added: 0010921
2014-02-11 15:38 frisch Note Added: 0010922
2014-02-19 20:20 doligez Tag Attached: patch
2014-04-02 23:05 frisch Note Added: 0011184
2014-04-03 00:52 yallop Note Added: 0011189
2014-04-03 12:03 frisch Note Added: 0011206
2014-04-05 11:17 gasche Note Added: 0011231
2014-04-07 17:36 frisch Note Added: 0011241


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker