typecore: a proper datatype for type_pat modes #9030

gasche · 2019-10-11T07:19:20Z

This type describes the parameter space of the [type_pat] function
(which type-checks of patterns, and in fact does quite a bit more) in
a way that also documents its behavior.

The code ends up being slightly more verbose at places: it's always
shorter to access one of four independent arguments than to go get the
information inside one record structure. But now it is clear which
parameters are meaningful in which situation, and I believe the code
is easier to read.

(cc @trefis @lpw25 @garrigue)

garrigue

Again, all this is extremely verbose. I think we will need a bit more time to converge, at least first agree on the comments, then see what is really the right API for this function.

typing/typecore.ml

garrigue · 2019-10-11T15:32:21Z

typing/typecore.ml

+   [counter_example_checking_info] contains various parameters for
+   this mode of operation. *)
+and counter_example_checking_info = {
+    explode: explosion_fuel;


Why use a custom type name here?
You could also name the field itself explosion_fuel.

I kept the name explode to reduce the changes in the type_pat codebase, and I used a custom type name to be able to consistently document each field at the place where the type is defined, rather than documenting the record field itself (I did that at first and the result was inconvenient).

For the record (no pun intended) I like @garrigue's suggestion better.
I'm not sure reducing the diff should be the goal here. Your aim is to make the code more readable, I think like it'd be slightly better if the field was named explosion_fuel rather than explode.

(Also, I have a personal dislike of type aliases, I think that most of their use are a mistake, this particular case being an example)

typing/typecore.ml

gasche · 2019-10-11T21:13:14Z

Concretely, here are some facts that were true about the previous code but very hard to decipher for someone not familiar with the implementation, and are now obvious with the new presentation:

constrs and labels were either None together or Some together (this was already clarified by your proposed In Typecore.type_pat, coalesce constrs and labels into map #9008 which is superseded by the present PR)
mode was always Normal when they were None, and the explode value was irrelevant in that case
Normal meant two different things depending on whether constrs/labels were None or Some

typing/typecore.ml

gasche · 2019-10-14T10:10:41Z

typing/typecore.ml

+         | exception Parmatch.Empty -> raise (Error (loc, !env, Empty_pattern))
+         | (sp, constrs, labels) ->
+            if sp.ppat_desc = Parsetree.Ppat_any then k' Tpat_any else
+            if must_backtrack_on_gadt then raise Need_backtrack else


This Need_backtrack should only be done if sp is a Ppat_or; in a further PR we should modify this code to match on sp.ppat_desc here (and deduce the new explode in passing).

trefis

I like this PR a lot! (And I do not find it too verbose.)

I left a bunch of stylistic comments (sorry!), but otherwise don't have much to say: the code seems fine, and @garrigue is in a much better position to validate the docstrings that you are adding.

typing/typecore.ml

gasche · 2019-10-14T14:56:53Z

( @trefis : Jacques and Florian offered to discuss the PR together and live-push extra patches to make it look better in Jacques' eyes. I'll do another pass when they're done (hopefully tomorrow) and will integrate your comments, thanks! )

typing/parmatch.mli

typing/typecore.ml

trefis · 2019-10-14T15:14:21Z

I'll do another pass when they're done (hopefully tomorrow) and will integrate your comments, thanks!

Ack.
Although I was too curious and already looked at the commits they just pushed (which contains a typo in its message btw)

garrigue

All is in the interaction...

garrigue · 2019-10-16T08:38:39Z

typing/typecore.ml

+    Parmatch does not use type information, so this pattern may exhibit two
+    issues:
+    - some parts of the pattern may be ill-typed due to GADTs.
+    - some wildcard patterns may not match any values: their type are empty.


Actually these two issues are not orthogonal.
Namely, when explode a wildcard we do not so much expect it to be empty, rather we expect that all the branches will result in equations that make the remainder of the pattern ill-typed.

In the context of this search program, "being well-typed" may have either a local or a global meaning. Local: it's well-typed as a program fragment in isolation. Global: it's well-typed inside the rest of the pattern. Because we are doing backtracking, the global meaning should be refined: there exists a typed form for the fragment such that invoking the search continuation with this form eventually succeeds. In the same style, "empty" here means that there is no well-typed value, globally: there is no value such that invoking the search continuation eventually succeeds.

(I don't think it's worth trying to express this nuance in this part of the documentation.)

garrigue · 2019-10-16T08:40:23Z

typing/typecore.ml

+  }
+(**
+    [explosion_fuel] controls the checking of wildcard patterns.
+    We eliminate potentially empty wildcard patterns by exploding them


ditto above, it is not so much the or-pattern that is empty, as the whole pattern once we have chosen a branch in the or-pattern

I added an extra comment on the splitting mode that talks (with examples) on the non-local nature of the search. I think it's enough to document it only there. I would claim that the subtlety you are pointing out is not due to wildcards in general, but in the or-patterns that some of those wildcards will explode into, so it's really related to or-patterns.

gasche · 2019-10-16T11:33:52Z

After Jacques' pass two days ago and Florian's pass yesterday, I did another pass in separate commits:

minor/local changes to slightly improve the writing of my esteemed colleagues
a new documentation comment on [splitting_mode] that explodes the non-local character of or-pattern choices (and consequently the important computational cost of backtracking)
a round of code changes to integrate @trefis' remarks

Is at least one person satisfied enough of the current state that they declare it good to merge?

typing/typecore.ml

trefis · 2019-10-16T12:04:36Z

typing/typecore.ml

+    The aim of [type_pat] in the [Counter_example] mode is to refine this
+    syntactic pattern into a well-typed pattern, and ensure that it matches
+    at least one concrete value.
+    - It filters ill-typed branches of or-patterns.
+      (see {!splitting_mode} below)
+    - It tries to check that wildcard patterns are non-empty.
+      (see {!explosion_fuel})


typing/typecore.ml

trefis

I left a few more comments, mostly for typos, and a couple of questions for things that are still unclear to me.

I'll also point out, because Gabriel is forcing my hand, that not only is the placement of docstrings suboptimal, it is also inconsistent: sometimes comments are above a definition, sometimes below. 😱

Nitpicks aside: this is a very nice PR!

gasche · 2019-10-16T14:31:30Z

@trefis I believe that I took care of all your comments (Thanks for the comments!)

trefis

LGTM.

typing/typecore.ml

Octachron · 2019-10-17T17:14:30Z

I am personally happy with the current PR (outside of the few last-minutes typos above).

gasche · 2019-10-17T20:42:27Z

Thanks to you both. I cleaned up the history as best as I could while preserving commit authorship. If the CI agrees I plan to merge tomorrow.

typing/typecore.ml

This type describes the parameter space of the [type_pat] function (which type-checks of patterns, and in fact does quite a bit more) in a way that also documents its behavior. The code ends up being slightly more verbose at places: it's always shorter to access one of four independent arguments than to go get the information inside one record structure. But now it is clear which parameters are meaningful in which situation, and I believe the code is easier to read. (This is joint work with Florian Angeletti)

…armatch

(spotted by Thomas Refis)

…th GADTs

gasche force-pushed the refactor-type_pat branch from b19c61a to 319f037 Compare October 11, 2019 10:47

gasche mentioned this pull request Oct 11, 2019

parmatch: don't rename idents when typing witnesses #9012

Closed

garrigue reviewed Oct 11, 2019

View reviewed changes

garrigue reviewed Oct 14, 2019

View reviewed changes

typing/typecore.ml Outdated Show resolved Hide resolved

gasche commented Oct 14, 2019

View reviewed changes

trefis reviewed Oct 14, 2019

View reviewed changes

typing/parmatch.mli Outdated Show resolved Hide resolved

typing/typecore.ml Outdated Show resolved Hide resolved

typing/typecore.ml Outdated Show resolved Hide resolved

garrigue reviewed Oct 16, 2019

View reviewed changes

gasche force-pushed the refactor-type_pat branch from 058c1e4 to 810692b Compare October 16, 2019 11:38

trefis reviewed Oct 16, 2019

View reviewed changes

typing/typecore.ml Outdated Show resolved Hide resolved

trefis reviewed Oct 16, 2019

View reviewed changes

typing/typecore.ml Outdated Show resolved Hide resolved

trefis reviewed Oct 16, 2019

View reviewed changes

typing/typecore.ml Outdated Show resolved Hide resolved

trefis reviewed Oct 16, 2019

View reviewed changes

typing/typecore.ml Outdated Show resolved Hide resolved

trefis reviewed Oct 16, 2019

View reviewed changes

trefis approved these changes Oct 17, 2019

View reviewed changes

Octachron reviewed Oct 17, 2019

View reviewed changes

typing/typecore.ml Outdated Show resolved Hide resolved

Octachron reviewed Oct 17, 2019

View reviewed changes

typing/typecore.ml Outdated Show resolved Hide resolved

gasche force-pushed the refactor-type_pat branch from 6b38f68 to c9f9673 Compare October 17, 2019 20:41

garrigue reviewed Oct 18, 2019

View reviewed changes

typing/typecore.ml Outdated Show resolved Hide resolved

gasche force-pushed the refactor-type_pat branch from c9f9673 to 5f2a069 Compare October 18, 2019 09:48

gasche and others added 2 commits October 18, 2019 11:50

typecore: change documentation of type_pat and add documentation to P…

4a3f427

…armatch

Octachron and others added 4 commits October 18, 2019 11:50

typecore: refine documentation for type_pat some more

15d452a

typecore: the documentation of Backtrack_or was wrong

767680f

(spotted by Thomas Refis)

typecore: another documentation pass (we are converging)

4c235bc

typecore: more explanations on the non-locality of type_pat search wi…

5f2a069

…th GADTs

gasche merged commit cc7231f into ocaml:trunk Oct 18, 2019

trefis mentioned this pull request Oct 21, 2019

In Typecore.type_pat, coalesce constrs and labels into map #9009

Closed

gasche mentioned this pull request Apr 12, 2022

Bad typer complexity (?) when checking that types are not directly recursive #11150

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

typecore: a proper datatype for type_pat modes #9030

typecore: a proper datatype for type_pat modes #9030

gasche commented Oct 11, 2019

garrigue left a comment

garrigue Oct 11, 2019

gasche Oct 11, 2019

trefis Oct 14, 2019

gasche commented Oct 11, 2019

gasche Oct 14, 2019

trefis left a comment

gasche commented Oct 14, 2019

trefis commented Oct 14, 2019

garrigue left a comment

garrigue Oct 16, 2019

gasche Oct 16, 2019

gasche Oct 16, 2019

garrigue Oct 16, 2019

gasche Oct 16, 2019

gasche commented Oct 16, 2019

trefis Oct 16, 2019

trefis left a comment

gasche commented Oct 16, 2019 •

edited

trefis left a comment

Octachron commented Oct 17, 2019

gasche commented Oct 17, 2019

typecore: a proper datatype for type_pat modes #9030

typecore: a proper datatype for type_pat modes #9030

Conversation

gasche commented Oct 11, 2019

garrigue left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

gasche commented Oct 11, 2019

Choose a reason for hiding this comment

trefis left a comment

Choose a reason for hiding this comment

gasche commented Oct 14, 2019

trefis commented Oct 14, 2019

garrigue left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

gasche commented Oct 16, 2019

Choose a reason for hiding this comment

trefis left a comment

Choose a reason for hiding this comment

gasche commented Oct 16, 2019 • edited

trefis left a comment

Choose a reason for hiding this comment

Octachron commented Oct 17, 2019

gasche commented Oct 17, 2019

gasche commented Oct 16, 2019 •

edited