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

Ambiguous pattern variables: add negative rows #1552

Merged
merged 5 commits into from Jan 9, 2018

Conversation

Projects
None yet
3 participants
@gasche
Copy link
Member

gasche commented Jan 1, 2018

Consider a set of pattern-matching clauses of the form

     | (Foo x, Foo y) -> ...
     | ((Foo x, _) | (_, Foo x)) when bar x -> ...

currently this code would raise a warning 57: the variable x in the guarded pattern ((Foo x, _) | (_, Foo x)) is ambiguous. However, this ambiguity is spurious, as the values that expose the ambiguity are of the shape (Foo v, Foo v'), and would all have been caught by the first clause.

This PR adds support for negative rows in the code computing stable pattern variables.

Note: Clauses that are guarded are not kept as negative clauses below (as we cannot reason on whether they catch values of the corresponding shape or not without analyzing the guard), so the following example would still raise a warning -- which I find slightly frustrating:

     | (Foo x, Foo y) when bar x || bar y -> ...
     | ((Foo x, _) | (_, Foo x)) when bar x -> ...

The first commit of this PR is a refactoring (that does not change the semantics) that I wrote as part of a larger PR to handle ill-typed columns in the ambiguous variable code (related to #1550, cc @trefis). In the inconsistent case, one needs to say that all variables are stable. We need to do the same in the case where we end up with an empty row to analyze but there remains a negative matrix -- filled with empty rows -- as this means that no value can ever reach this sub-matrix.

@trefis
Copy link
Contributor

trefis left a comment

The first commit is correct and indeed makes the situation nicer for my PR interested in coherence of the first column.

The second commit however seems incorrect. I'm tempted to believe the general idea is sound and that you only need to be a bit more careful in the implementation. But we'll see.

| { default; constrs = [] } ->
(* the first column contains no head constructor;
they are all _ after simplification, so it can be dropped *)
let default_ns = List.map snd ns in

This comment has been minimized.

@trefis

trefis Jan 2, 2018

Contributor

That line looks fishy.

I spent a long time thinking about the coherence implications of that line, that is: clearly the default_ns (which seems like a bad name to me btw, default_ns is in no way the default matrix of ns) you produce can contain incoherences, but does it matter?
I'm still not quite sure but I believe it does and that we should care about the coherence of ns.
Here we probably want to build the specialized submatrices of ns and recurse on each of them (keep default for the other argument on each of the recursive call). This is just an intuition however and it will be easier to test out if this PR is rebased on top of mine.

In any case, I took some time to produce a convoluted example introducing incoherence in specific places and trying to see how the new implementation would behave on it. At which point I realized I could greatly simplify my test case to the following code (where all the columns are coherent at every step):

type a = A1 | A2

type 'a alg =
  | Val of 'a
  | Binop of 'a alg * 'a alg

let cmp (pred : a -> bool) (x : a alg) (y : a alg) =
  match x, y with
  | Val A1, Val A1 -> ()
  | Val x, _
  | _, Val x when pred x -> ()
  | _, _ -> ()

With your implementation the warning doesn't trigger on this example. I think it should.

I tried the idea I mentioned above (recursing on each of the specialized submatrices of ns) and it does warn on that specific example (make core then ./boot/ocamlrun ./ocamlc -nostdlib -nopervasives -w +57 simple_amb.ml) but make world.opt fails because of the assert (ns = []) a few lines above.
So my implementation is not quite right either, but you can probably get something along this line working.

This comment has been minimized.

@trefis

trefis Jan 2, 2018

Contributor

The diff of my attempt is the following btw:

diff --git a/typing/parmatch.ml b/typing/parmatch.ml
index 16949df57..3fbac8c43 100644
--- a/typing/parmatch.ml
+++ b/typing/parmatch.ml
@@ -2195,8 +2195,17 @@ let rec matrix_stable_vars ns rs = match ns, rs with
     | { default; constrs = [] } ->
         (* the first column contains no head constructor;
            they are all _ after simplification, so it can be dropped *)
-        let default_ns = List.map snd ns in
-        matrix_stable_vars default_ns default
+        let q0_ns = discr_pat omega ns in
+        begin match build_specialized_submatrices ~extend_row:(@) q0_ns ns with
+        | { default = default_ns ; constrs = [] } ->
+          matrix_stable_vars default_ns default
+        | { default = _; constrs = constrs_ns } ->
+          let submat_stable =
+            List.map (fun (_, sub_ns) -> matrix_stable_vars sub_ns default)
+              constrs_ns
+          in
+          List.fold_left stable_inter All submat_stable
+        end
     | { default = _; constrs } ->
         (* A stable variable must be stable in each submatrix.
 

This comment has been minimized.

@gasche

gasche Jan 2, 2018

Author Member

(fun (_, sub_ns) -> matrix_stable_vars sub_ns default) does not respect arity, as sub_ns may in general have more columns than ns (while default always has one less). In the non-default case here it is safer build the specialized matrix of rs against the head of each constr_ns group (so to drop the decomposition of rs), which suggests that we are really trying to split on both matrices at once instead of decomposing them independently. Also it is not clear whether it is right to forget about default_ns in that case (when constrs_ns is non-empty): default_ns has less content than any constrs_ns, but precisely having less negative information can lead to accepting more positive rows, and thus finding unstable variables.

@gasche

This comment has been minimized.

Copy link
Member Author

gasche commented Jan 2, 2018

Thanks, indeed List.map snd ... is not right -- I'm not sure why I thought it would work.

Regarding the first commit, that it is the only one that I suggested that you could cherry-pick into #1550 -- not the second commit which indeed is independent.

This code is non-trivial to write because it is the only one where we have both a negative matrix and a positive matrix. In other functions (for example the satisfiable variables) we have only a positive row, and then they work by specializing the negative matrix in each case. Here we need to do a cross-product, splitting submatrices for both matrices -- or we could have done only a single split on the joint matrix, but this would require API changes and is hard with different row types.

The reason why the other functions get away with only a positive row (instead of the general case of a positive matrix) is that they have an easy operation to join the results of two "parallel" calls, the calls on the two sides of an or-pattern (for satisfiable the join is just ||). I don't know (it is not obvious) whether this function can be rewritten in this style.

I think I'll wait until #1550 is merged to make another iteration on this PR, taking your comments/suggestions into account.

@gasche gasche force-pushed the gasche:ambiguous-variables-negatives branch from 2186cb5 to b8785f6 Jan 3, 2018

@gasche

This comment has been minimized.

Copy link
Member Author

gasche commented Jan 3, 2018

@trefis: I just rebased this PR, and I changed the algorithm to split on all rows (positive and negative) at the same time -- kind of cool. Let me know what you think.

(I have left the handling of the default matrix in the non-empty-constrs case unchanged, while it is not completely clear to me that it is actually correct. But I think it is.)

@trefis
Copy link
Contributor

trefis left a comment

The code is surprisingly simpler than I would have expected! :)

However, trying it on the example I gave during the previous round of review (that github now hides) I still get no warning.
Can you confirm whether you agree or not that a warning should be emitted?
And regardless of the answer, do you mind adding it to the testsuite?

For reference, the test case was:

type a = A1 | A2

type 'a alg =
  | Val of 'a
  | Binop of 'a alg * 'a alg

let cmp (pred : a -> bool) (x : a alg) (y : a alg) =
  match x, y with
  | Val A1, Val A1 -> ()
  | Val x, _
  | _, Val x when pred x -> ()
  | _, _ -> ()
@@ -1558,21 +1558,14 @@ and push_no_or_column rs = List.map push_no_or rs
(* Those are adaptations of the previous homonymous functions that

This comment has been minimized.

@trefis

trefis Jan 3, 2018

Contributor

That comment should be updated (or simply removed?), you're only "adapting" one function, and its name is different.

To track this information, the matrices we analyze contain both *positive* rows,
that describe the rows currently being analyzed (of type amb_row, so that their
varsets are tracked) and *negative rows*, that describe the cases already
matched against. A variable is stable if there exist two values that

This comment has been minimized.

@trefis

trefis Jan 3, 2018

Contributor

I think you meant "unstable" here?

@trefis

This comment has been minimized.

Copy link
Contributor

trefis commented Jan 3, 2018

OK, I think I know what the issue is:

In the case where constrs is not nil, you say:

If the first column contains some head constructors, there
is no need to look at stability for the default matrix: all
other submatrices contain the default matrix, so they have
less stable variables.

But that's actually wrong.
The default matrix might also contain fewer negative rows, and so it might contain more unstable variables!

@trefis

This comment has been minimized.

Copy link
Contributor

trefis commented Jan 3, 2018

On the example I have given, the problem appears as follow

neg | Val A1    Val A1 |
pos | Val x     _      |
pos | _         Val x  |

Which will be split into:

            neg | A1   Val A1 |
constrs = [ pos | _    _      | ]
            pos | _    Val x  |

default = pos | _   _     |
          pos | _   Val x |

And then you recurse only on constrs (note that recursing on this first default matrix would have given you a warning I believe).

Which is further split into:

            neg | Val A1 |
constrs = [ pos | _      | ]
            pos | Val x  |

default = pos | _     |
          pos | Val x |

And again:

            neg | A1 |
constrs = [ pos | _  | ]
            pos | _  |

default = pos | _ |
          pos | _ |

And one last time:

            neg | |
constrs = [ pos | | ]
            pos | |

default = pos | |
          pos | |

At which point when you recurse on the only constrs matrix you say "oh I have a negative row, all the variables must be stable!".

The thing that is a bit sad is that if we recurse on the default matrix as well as on the constrs matrices, we will get the warning even if A1 is alone in its signature.
But I don't see any easy way around that. Perhaps simplify_head_amb_pat_* could check if a constructor is alone in its signature and replace it by omega but that seems britle, and doesn't extend well ("signature" is too loosely defined in our untyped world)

@trefis

This comment has been minimized.

Copy link
Contributor

trefis commented Jan 3, 2018

Also, I meant to say: simplify_first_amb_col reads to me like "simplify the first ambiguous column" which is not what's going on.

How about introducing submodules which will contain a "row" type and the correspond simplification functions?

@trefis

This comment has been minimized.

Copy link
Contributor

trefis commented Jan 3, 2018

At which point when you recurse on the only constrs matrix you say "oh I have a negative row, all the variables must be stable!".

The thing that is a bit sad is that if we recurse on the default matrix as well as on the constrs matrices, we will get the warning even if A1 is alone in its signature.

Actually, that hints at the fact that we probably want to call full_match to decide whether we want to consider the default matrix or the specialized submatrices.
I'll let you check it out, I'm done for today!

@gasche

This comment has been minimized.

Copy link
Member Author

gasche commented Jan 3, 2018

Excellent observations and interesting feedback -- as I am getting used to. Thanks!

@gasche gasche force-pushed the gasche:ambiguous-variables-negatives branch from b8785f6 to a10bff1 Jan 4, 2018

@gasche

This comment has been minimized.

Copy link
Member Author

gasche commented Jan 4, 2018

I made a first batch of easy changes that addresses some of your comment (and optimizes the special case where there is no positive row left in the matrix). In particular, I believe that the default issue is fixed in the most natural (and least clever) way, by defining submatrices as default :: List.map snd constrs. Feedback is welcome. I plan to use your suggestion of sub-modules and propose this change later in the day.

@gasche

This comment has been minimized.

Copy link
Member Author

gasche commented Jan 4, 2018

(I'm also interested in playing with full_match, we'll see.)

@gasche

This comment has been minimized.

Copy link
Member Author

gasche commented Jan 4, 2018

I just pushed a new commit that uses full_match in a surprisingly simple way (minor point, but it's a bit annoying that full_match [] raises an assert false instead of returning false) that I believe is correct. I use your testcase with type a = A1;; to check that the behavior you expect works.

@trefis

This comment has been minimized.

Copy link
Contributor

trefis commented Jan 4, 2018

I think I agree with you that the current implementation is correct.

I'll resume nitpicking then:

  • some (comment) lines are over 80c

  • in one of the base cases of the algorithm you say:

    if at least one row is negative, the matrix matches no value

    this is poorly formulated (the matrix does match some values, doesn't it?), I'd go with something along the line of "if the matrix still has a negative row, that row will match before any positive one", and I'd move the comment to the place where we catch the exception and return All.

@gasche

This comment has been minimized.

Copy link
Member Author

gasche commented Jan 4, 2018

in one of the base cases of the algorithm you say:

if at least one row is negative, the matrix matches no value

this is poorly formulated (the matrix does match some values, doesn't it?), I'd go with something along the line of "if the matrix still has a negative row, that row will match before any positive one", and I'd move the comment to the place where we catch the exception and return All.

I think we are misunderstanding each other here and we should dig in. The comment is there (only) in the case where the rows are empty (a non-empty matrix with several empty rows). One or several empty positive rows matches exactly one vector of values (the empty vector), but the presence of a negative row means that this empty vector is rejected, so the matrix matches nothing.

that row will match before any positive one

Note that, in matrix_stable_vars, I don't consider an order between the rows -- the result of the function does not depend on the row order. For the positive rows, stability is precisely about computing who doesn't depend on the matching order. For the negative rows, the idea is that the value space is the same no matter what the order is. In practice, I think that the order is preserved (negative rows start at the top, and I think they stay at the top), but the semantics of the function is that a negative row anywhere kills this sub-space of values before they reach any of the positive rows.

@gasche

This comment has been minimized.

Copy link
Member Author

gasche commented Jan 4, 2018

(Most other functions in Parmatch have this characteristic that they are insensitive to the row order. The order comes in in the choice of who is pss and who is rs.)

@gasche

This comment has been minimized.

Copy link
Member Author

gasche commented Jan 4, 2018

@trefis two points:

  • The Module-using change is rather invasive, in part because it encourages me to indent larger blocks of code. I would prefer to do it as a separate PR, so that it does not trash the whole diff, either before we try to merge this PR or after it.

  • I think that you are moving from the spot of "reviewer" to the spot of "co-author" in the (yet unwritten) Changes entry, which means that we need @maranget to review it when we both agree that we like the current state.

@gasche gasche force-pushed the gasche:ambiguous-variables-negatives branch from b843e58 to 3e2a642 Jan 4, 2018

@trefis

This comment has been minimized.

Copy link
Contributor

trefis commented Jan 4, 2018

  • Delaying the renaming / introduction of modules sounds fine.
  • Having Luc review this is obviously a good idea, regardless of my "spot" :)

Going back to the discussion about ordering and such:
When you arrive on a matrix with no columns but at least one (and potentially more) row then they are all matching the same empty vector (if you ignore the polarity of the row), I think we both agree on that.

Now, I guess your interpretation of the polarity in some way leads you to saying that "if I have a negative row, then the matrix doesn't filter the empty vector": you are changing the definition of what it means for a matrix to filter a value in presence of polarity. That might be fine, but I wasn't reasoning about it in the same way and it is also never made explicit in your documentation/comments (but of course I might have missed the relevant comment).

The way I was thinking about it was more in line with the other comments you've placed in the code (on the definition of signed):

To track this information, the matrices we analyze contain both positive rows,
that describe the rows currently being analyzed (of type amb_row, so that their
varsets are tracked) and negative rows, that describe the cases already
matched against.

Indeed even though in the matrix the rows order is irrelevant (and not guaranteed) the guarantee you have is we consider the clauses of the pattern matching in order, and grow our set of negative rows as we go.

I see this as coherent with the last part of your message above, i.e.

For the negative rows, the idea is that the value space is the same no matter what the order is.
[...] the semantics of the function is that a negative row anywhere kills this sub-space of values before they reach any of the positive rows.

which is what I was roughly trying to express previously.

Does that make sense?

@maranget
Copy link
Contributor

maranget left a comment

Fine idea to introduce negative rows, as it leads nice code sharing.

parmatch.ml: refactor the simplify_first_col and simplify_head_pat fu…
…nctions

This is necessary to use several distinct simplify_first_col at once,
as we wish to do to handle negative rows in matrix_stable_vars.

@gasche gasche force-pushed the gasche:ambiguous-variables-negatives branch from 3e2a642 to 6e41d65 Jan 9, 2018

@gasche

This comment has been minimized.

Copy link
Member Author

gasche commented Jan 9, 2018

I made two small changes suggested by Luc during his review:

  • the optimization of all-negative rows is implemented by an if instead of a when
  • the construction of the initial matrix in pattern_stable_vars is written in a slightly
    different way that restores the expected row order (the row order is irrelevant in
    the algorithm, but we can still finesse about it)

Edit: the plan is to merge the PR if the CI passes. @trefis, if you wish to tell Github that the changes you requested have been performed, now is the time.

@trefis

trefis approved these changes Jan 9, 2018

Copy link
Contributor

trefis left a comment

All the bugs/issues have been fixed and I think we're all happy with the code changes.

Personally I'd still change the comment we discussed in our last exchange as nothing in the file explains it, and I believe it could be formulated in another way which doesn't require extra knowledge.
That said, it's not really important and I wouldn't be very sad if you merged as is.
(N.B. I assumed we agreed on my last message which you haven't replied to)

| [] -> All
| ((Positive {row = []; _} | Negative []) :: _) as empty_rows ->
let exception Negative_empty_row in
(* if at least one empty row is negative, the matrix matches no value *)

This comment has been minimized.

@trefis

trefis Jan 9, 2018

Contributor

No change to that comment then?

@gasche

This comment has been minimized.

Copy link
Member Author

gasche commented Jan 9, 2018

Sorry, I forgot to change that comment. I will do this soon, before merging -- currently I am rebasing #1560 and #1561 against this one.

@gasche

This comment has been minimized.

Copy link
Member Author

gasche commented Jan 9, 2018

@trefis thinking about this more, I think that it is correct to say explicitly that the semantics of a signed matrix is different from the semantics of a non-signed matrix: their set-of-values interpretation is not the same. To this end, I amended the comment introducing signed as follows:

    To track this information, the matrices we analyze contain both
    *positive* rows, that describe the rows currently being analyzed
-   (of type amb_row, so that their varsets are tracked) and *negative
-   rows*, that describe the cases already matched against. A variable
-   is stable if, for any value not matched by any of the negative
-   rows, the environment captured by any of the matching positive rows
-   is identical.
+   (of type Varsets.row, so that their varsets are tracked) and
+   *negative rows*, that describe the cases already matched against.
+
+   The values matched by a signed matrix are the values matched by
+   some of the positive rows but none of the negative rows. In
+   particular, a variable is stable if, for any value not matched by
+   any of the negative rows, the environment captured by any of the
+   matching positive rows is identical.
 *)
 type ('a, 'b) signed = Positive of 'a | Negative of 'b

I believe that the comment in the function itself is now correct with respect to that interpretation.

(Maybe it would be even clearer to explicitly distinguish the "semantics as a matrix" and the "semantics as a signed matrix" (the signed semantics), and say something like "the signed semantics of m is empty" or at least "the signed matrix m is empty".)

@gasche gasche force-pushed the gasche:ambiguous-variables-negatives branch from 6e41d65 to f0f985b Jan 9, 2018

@trefis

This comment has been minimized.

Copy link
Contributor

trefis commented Jan 9, 2018

thinking about this more, I think that it is correct to say explicitly that the semantics of a signed matrix is different from the semantics of a non-signed matrix: their set-of-values interpretation is not the same.

Yep, that's the other way to fix "the issue".
I have no problem with that option: as long are the comments are all consistent, I'll be happy.

Your new comment on signed seems enough indeed. I'd be curious to see your "more explicit" version, but probably you can keep it for the paper you'll surely write about this.

@gasche gasche merged commit c9469ca into ocaml:trunk Jan 9, 2018

2 checks passed

continuous-integration/appveyor/pr AppVeyor build succeeded
Details
continuous-integration/travis-ci/pr The Travis CI build passed
Details
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
You can’t perform that action at this time.
You signed in with another tab or window. Reload to refresh your session. You signed out in another tab or window. Reload to refresh your session.