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

Binding variables in disjunctive patterns #6901

Closed
vicuna opened this issue Jun 11, 2015 · 12 comments
Closed

Binding variables in disjunctive patterns #6901

vicuna opened this issue Jun 11, 2015 · 12 comments

Comments

@vicuna
Copy link

vicuna commented Jun 11, 2015

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:

function
   K1 with n=0
 | K2 n ->  .... n .....
 | K3 -> ...

I believe that the compiler could generate efficient code for this case.

Current workarounds:

  1. Duplication of the right-hand-side code

    function
       K1 -> .... 0 ....
     | K2 n -> .... n ...
     | K3 -> ...

    Bad for obvious reasons.

  2. Duplicate the pattern match.

     function
       (K1 | K2 _) as x ->
         let n = match x with K1 -> 0 | K2 n -> n | _ -> assert false in
          .... n ...
     | K3 -> ...

    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:

let rec unif x y =
 match x,y with
    Var r, _ when !r != None -> unif (deref f []) y
  | App(Var r,args),_ when !r != None -> unif (deref f args) y
  | ...

I have faced similar snippets of code in the implementation of Coq, Matita and
a lambda-prolog interpreter we are writing.

@vicuna
Copy link
Author

vicuna commented Jun 12, 2015

Comment author: @alainfrisch

Another work-around is to share the common code:

  let k n  = ... in
  match ... with 
   | K1 -> k 0
   | K2 n -> k n
   | K3 -> ...

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

  try match ... with
    | K1 -> raise (`K 0)
    | K2 n -> raise (`K n)
    | K3 -> ...
  with `K n -> ...

@vicuna
Copy link
Author

vicuna commented Jun 12, 2015

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.

@vicuna
Copy link
Author

vicuna commented Jun 12, 2015

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

@vicuna
Copy link
Author

vicuna commented Jun 15, 2015

Comment author: @alainfrisch

it's quite easy to implement this optimization

For the records, the patch can be found here: #6242

@vicuna
Copy link
Author

vicuna commented Jun 25, 2015

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

@vicuna
Copy link
Author

vicuna commented Jun 25, 2015

Comment author: @alainfrisch

In the "with" case, whether the branch is taken or not does not depend on the value assigned by "with"

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

@vicuna
Copy link
Author

vicuna commented Jun 25, 2015

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:
https://wiki.haskell.org/Pattern_guard

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

@vicuna
Copy link
Author

vicuna commented Jun 25, 2015

Comment author: @yallop

Would nested 'with' and non-exhaustive patterns introduce any additional problems besides the existing issues with lazy patterns and 'when' guards?

@recoules
Copy link

recoules commented Aug 26, 2019

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

@gasche
Copy link
Member

gasche commented Aug 28, 2019

I made a related design proposal (draft) on the last 1st of April.

@github-actions
Copy link

github-actions bot commented Dec 4, 2020

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.

@github-actions github-actions bot added the Stale label Dec 4, 2020
@gasche gasche removed the Stale label Dec 4, 2020
@github-actions
Copy link

github-actions bot commented Dec 6, 2021

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.

@github-actions github-actions bot added the Stale label Dec 6, 2021
@github-actions github-actions bot closed this as completed Jan 7, 2022
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

4 participants