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
Binding variables in disjunctive patterns #6901
Comments
Comment author: @alainfrisch Another work-around is to share the common code:
Ideally, the compiler would detect that the only references to [k] are full applications in tail context within its scope and compile that as a "static handlers" (with the support introduced in #5879) to avoid any runtime cost. Btw, it's quite easy to implement this optimization in simplif.ml, for instance (I had written that code once...). The optimization would produce the same as for (using the syntax from #5879):
|
Comment author: sacerdot I did not mention this other work-around because of efficiency (solved by static handlers), but also because it moves the code far away. I like to be able to understand the code of my function at-a-glance, without having to introduce several _aux functions defined elsewhere just for technical reasons. |
Comment author: @alainfrisch That's true, and I'm not necessarily against extensions of pattern matching (also with guards under or-patterns). But these extensions are always tricky, with uncertain semantics (expressions for guards or default values can modify parts of the matched expression). |
Comment author: @alainfrisch
For the records, the patch can be found here: #6242 |
Comment author: @gasche Note that there is an important difference between this proposal | K with n = 0 -> ... and the more general pattern guards | K when (Some v) = Map.find_opt ... -> ... In the "with" case, whether the branch is taken or not does not depend on the value assigned by "with", so the with right-hand-side does not need to be evaluated during pattern-matching -- evaluation can be delayed until the branch is effectively taken. On the other case of general patter guards, whether the branch is taken depends on the value of the exception which needs to be forced during matching, raising the same potential issues as (lazy pattern). |
Comment author: @alainfrisch
I don't see the difference, both "with" bindings and "when" guards can be executed between the structural matching and before the action, and both can mutate variables or raise exceptions. In particular, since the when guard can depend on with-bound variables, these bindings can affect the decision: | ((x, None) with y = 0 | (x, Some y)) when x < y -> ... |
Comment author: @gasche I was unclear in my comment above. I am not talking of the severely limited "when guards" as they exist in OCaml today, but the more expressive "pattern guards" as implemented in GHC: The problem you point out is inherent to the semantics of "when guard" today (they evaluation expressions and may affect branch-taking decisions), and is not made any better or worse with the suggested "with". On the contrary, having the ability to write non-exhaustive patterns as left-hand-side of "with" and have a non-matching semantics that skips the branch would introduce the same kind of issues we have with "when" today, even possibly worse as it could be checked deep in a pattern. ("with" doesn't really make sense if it's not accepted inside disjunctive patterns). |
Comment author: @yallop Would nested 'with' and non-exhaustive patterns introduce any additional problems besides the existing issues with lazy patterns and 'when' guards? |
This thread is pretty old... (may it live in another place?) The fact is I'm looking for this kind of feature and I'm wondering if it could not be implemented by restricting the right hand side expression to be, either an identifier or a constant (including everything pattern-matchable: immediate, constructor, etc...) Thus, the extension cannot interfere with the branch-taking decisions, can it? Example: immediate function
| K0 with n = 0
| Kn n -> foo n Example: identifier function
| K0 with n = Z.zero
| Kn n -> foo n or even let n = bar a b c d in
function
| K0 with n (* refer to the scope *)
| Kn n -> foo n |
I made a related design proposal (draft) on the last 1st of April. |
This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc. |
This issue has been open one year with no activity. Consequently, it is being marked with the "stale" label. What this means is that the issue will be automatically closed in 30 days unless more comments are added or the "stale" label is removed. Comments that provide new information on the issue are especially welcome: is it still reproducible? did it appear in other contexts? how critical is it? etc. |
Original bug ID: 6901
Reporter: sacerdot
Status: acknowledged (set by @damiendoligez on 2015-06-15T15:39:11Z)
Resolution: open
Priority: normal
Severity: feature
Version: 4.02.1
Category: language features
Monitored by: @gasche @yallop
Bug description
This is a feature request for allowing to bind a variable in a disjunctive pattern (for example using a with keyword). Example:
I believe that the compiler could generate efficient code for this case.
Current workarounds:
Duplication of the right-hand-side code
Bad for obvious reasons.
Duplicate the pattern match.
The generated code really performs the pattern match twice and is therefore inefficient.
Frequency: this situation happens very often, for example when writing unification/type checking code. Real code example:
I have faced similar snippets of code in the implementation of Coq, Matita and
a lambda-prolog interpreter we are writing.
The text was updated successfully, but these errors were encountered: