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

Allow type-based selection of GADTs constructors #1648

Merged
merged 1 commit into from Mar 12, 2018

Conversation

Projects
None yet
5 participants
@trefis
Copy link
Contributor

trefis commented Mar 6, 2018

This is a very straightforward change now that all the bugs which prevented this modification have been fixed.
I have tested this on Jane Street's codebase, and it compiles fine. That didn't use to be the case: building that codebase with this patch, I encountered various issues which have been fixed by #1620 (this was a well known blocker, which had already been pointed out in MPR#7298) and #1583 .

As for the performance implications, I do not have much to report about Jane Street codebase (there is simply no noticeable change to compilation time).
The same cannot be said for the compiler itself: while the difference is lost in the noise when you do a parallel build, doing a sequential one will take about 10% longer on average.

I didn't manage to confirm that any particular point of type_cases is responsible for any substantial portion of the slow down (although I do suspect the call to duplicate_ident_types at the top).
I'll most likely investigate this more at some point in the future, but meanwhile I think it might make sense to merge this simple patch, and that we can probably bear the regression.

@gasche
Copy link
Member

gasche left a comment

The patch is perplexing to me (someone that knows very little about the type-checker implementation) because I don't understand how most of the proposed changes are related to the PR goals and why they are necessary (or even good ideas).

As I understand it, your PR does three things:

  1. there was a bunch of logic in disambiguate to raise an error on GADT constructors (the weirdly named check_lk business) which you got rid of. That sounds reasonable and clearly related to your goal. Why isn't this change enough?

  2. You change the notion of contains_gadt (a check on patterns) to be more restrictive in an apparently sensible sense: it now says "yes" only if one of the constructors involved in the pattern is generalized (adds existentials or equations), instead of saying yes if a non-generalized constructor of a type that contains generalized constructors is involved. Why not. But why is this change necessary here?

  3. In type_cases you turn a lot of the "if has_gadts then do complex level-handling stuff" into "if has_constructors then do complex level-handling stuff". I have no idea how that is related to allowing disambiguation of GADT constructors, and it sounds like a weird change to me: we can expect that the complex GADT-only code paths are less well-tested than the others, so running them for virtually all patterns tomorrow is bound to raise unattended issue -- and sure enough, you report that you had to fix various problems before this change worked, which I guess means that running complex paths more often can be good.

Changes (2) and (3) may be good ideas (I can see why (2) would be, but (3) smells very strange to me), but I would find it reassuring to understand how they relate to disambiguating GADTs.

@@ -2557,22 +2549,22 @@ let contains_polymorphic_variant p =
in
try loop p; false with Exit -> true

let contains_gadt env p =
let rec loop env p =
let contains_gadt p =

This comment has been minimized.

@gasche

gasche Mar 6, 2018

Member

If I understand correctly, the semantics of contains_gadt changed, right? Before it would check if some constructors in the pattern where part of a "GADT type" (a type with at least one constructor adding existentials or equations to the context), and now it checks whether a constructor is a "generalized constructor" (it adds existentials or equations itself).

Do you know if there is any situation where the difference between the two meanings matter? (Why wasn't your simpler definition written in the first place?)

This comment has been minimized.

@lpw25

lpw25 Mar 6, 2018

Contributor

Before it would check if some constructors in the pattern where part of a "GADT type"

That's not what lookup_all_constructors does. It looks up all the constructors in the environment with the same name. So the check used to return true if any of the constructors with that name in scope was a GADT. The function now operates on the typedtree, after disambiguation, and so already knows which of the constructors was selected.

@alainfrisch

This comment has been minimized.

Copy link
Contributor

alainfrisch commented Mar 6, 2018

I believe this is about addressing https://caml.inria.fr/mantis/view.php?id=6023, right?

@lpw25

This comment has been minimized.

Copy link
Contributor

lpw25 commented Mar 6, 2018

but (3) smells very strange to me

(3) is the main part of the patch. The only reason we don't disambiguate GADTs already is that has_gadts gives the wrong answer in the presence of disambiguation -- and by the time we find out it was wrong it is too late to go back and use the GADT path. Whereas has_constructors is correct in the presence of disambiguation.

@gasche

This comment has been minimized.

Copy link
Member

gasche commented Mar 6, 2018

That clarifies things a bit, thanks.

Maybe in that case may_have_gadts would be a better name than has_constructor in type_cases, and there could be a comment giving Leo's explanation at this declaration site.

Also, is the contains_gadt function actually still useful in that case? (What is the use-case where we have a pattern and we know for sure that disambiguation already happened?) Shouldn't it be completely replaced by contain_constructor, to be renamed may_contain_gadts?

Edit: I see from Leo's last comment #1648 (comment) that my questions here were again too naive. Those points might again deserve a comment.

@trefis

This comment has been minimized.

Copy link
Contributor Author

trefis commented Mar 6, 2018

I believe this is about addressing https://caml.inria.fr/mantis/view.php?id=6023, right?

Correct, I'll add that in Changes.

Maybe in that case may_have_gadts would be a better name than has_constructor in type_cases, and there could be a comment giving Leo's explanation at this declaration site.

I don't mind doing such a change.

Also, is the contains_gadt function actually still useful in that case? (What is the use-case where we have a pattern and we know for sure that disambiguation already happened?) Shouldn't it be completely replaced by contain_constructor, to be renamed may_contain_gadts?

It is used when typechecking the rh-side of the various clauses. One could avoid it and simply reuse the previously computed variable but that would be less precise.

@alainfrisch alainfrisch changed the title Disambiguate gadts Allow type-based selection of GADTs constructors Mar 6, 2018

@alainfrisch

This comment has been minimized.

Copy link
Contributor

alainfrisch commented Mar 6, 2018

Thanks for the confirmation. I've changed the PR title to something more explicit. (Feel free to change back if you don't agree.)

@trefis trefis force-pushed the trefis:disambiguate-gadts branch from b80bcc5 to de49ff1 Mar 6, 2018

@alainfrisch

This comment has been minimized.

Copy link
Contributor

alainfrisch commented Mar 6, 2018

doing a sequential one will take about 10% longer on average.

This is surprising, given that the compiler does not contain a lot of GADTs (mostly format strings, I believe).
Does the PR impacts significantly the way code without GADT is type-checked?

@gasche

This comment has been minimized.

Copy link
Member

gasche commented Mar 6, 2018

Yes, all patterns with variant constructors now go through the GADT path -- as they may be understood to contain GADTs during pattern type-checking thanks to disambiguation information.

However, because of disambiguation, we can't know for sure whether the
patterns contain some GADT constructors. So we conservatively assume that
any constructor might be a GADT constructor. *)
let may_contain_gadts = List.exists contains_constructor patterns in

This comment has been minimized.

@gasche

gasche Mar 7, 2018

Member

I like this patch but I think that you may go even further and rename contains_constructor into may_contain_gadts, and call the local boolean has_gadts again (or may_have_gadts if you wish). This would make other call sites, such as the Pexp_let one, easier to follow.

This comment has been minimized.

@trefis

trefis Mar 7, 2018

Author Contributor

I guess I could rename the function and move the comment to its definition. I don't like has_gadts but may_have_gadts would be fine if you prefer that over contain.

This comment has been minimized.

@gasche

gasche Mar 7, 2018

Member

I have no opinion over have/has vs contain/contains, just that the toplevel function name could express that it's actually used to look for potential gadts. No opinion on what the local variable name should be (as long as it doesn't shadow the function name, that's ugly) -- reusing has_gadts had the advantage of a smaller diff but that does not matter so much.

@trefis

This comment has been minimized.

Copy link
Contributor Author

trefis commented Mar 7, 2018

Btw @gasche , @alainfrisch : could I get your thoughts on the performance implications? Or even better some numbers about the compile time of your preferred codebase with a version of the compiler including this patch.

@alainfrisch

This comment has been minimized.

Copy link
Contributor

alainfrisch commented Mar 7, 2018

10% more time on the whole sequential compilation: is that for bytecode only, for bytecode + native? Just compiling the compiler, or everything in the distribution? Globally, this seems not negligible and suggest that (i) resolution of constructors itself (which should not account for a large fraction of the total) has become probably an order of magnitude slower; (ii) the slowdown on some specific kinds of code might be dramatic. So I'd be careful. Do you have a clear intuition on why the new code path is significantly slower?

@garrigue

This comment has been minimized.

Copy link
Contributor

garrigue commented Mar 8, 2018

The overhead suggests that it might be worth considering backtracking code in this case (i.e. first try the simple code code path, and backtrack and use the gadt code path if we end up having to add an equation).
This shouldn't be difficult.

@garrigue

This comment has been minimized.

Copy link
Contributor

garrigue commented Mar 8, 2018

And again I suggest you provide a full explanation of what your code is doing, how, and why so.
It should make reviewing, and be useful as future reference when reading the code.
By the way this raises the question of what to do with the information in merged PRs.
Should we keep pointers to the PRs in the code, for future reference?

@trefis

This comment has been minimized.

Copy link
Contributor Author

trefis commented Mar 8, 2018

10% more time on the whole sequential compilation: is that for bytecode only, for bytecode + native? Just compiling the compiler, or everything in the distribution?

That was for world.opt, but measured with time which doesn't give the most stable results.
To have a better ground for discussion I now rebuilt world.opt with -dtimings 10 times for both trunk and this GPR.
The (averaged) results are available here.
It appears I had jumped to conclusions too quickly when looking at the output of time, the slow down appears to be less than 1% on the distribution.

People willing to reproduce this "benchmark" might want to apply a slight variation of this patch on the various Makefiles of the distribution.
Where my_run.sh is simply:

#!/bin/bash

"$@" >> /tmp/dtimings

This is of course a very rough benchmarks and I welcome any other measurement.

For the record: I don't think "resolution of constructors" has gotten any slower in this PR.
As I had said in my first message, my intuition is that the now more frequent call to duplicate_ident_types is probably responsible for a good chunk of this actually negligible slow down.

@garrigue

This comment has been minimized.

Copy link
Contributor

garrigue commented Mar 9, 2018

I checked again with just make partialclean; time make all after bootstrapping. The results seem coherent with yours: there is a slowdown, but less than 1%.
So this may not be so significant. (Still, if we add 1% by PR dozens of time, this may become significant...)
The other reason to delay this change was that the GADT path was not so well exercised, but after all these years this is no longer the case.
Still need to review this properly.
By the way, I can understand the interaction with #1583, but much less with #1620.

@trefis

This comment has been minimized.

Copy link
Contributor Author

trefis commented Mar 9, 2018

For the interaction with #1620, have a look at the following test I added in that GPR, and in particular at the difference with the very similar test a few lines above using a non GADT constructor.

Before #1620 , if we had merged the code paths as is done here, then both examples would have been rejected.
The fixes done in #1620 make it so that both are accepted, and we can now merge the code paths without worry.

@@ -4660,7 +4654,7 @@ and type_cases ?in_function env ty_arg ty_res partial_flag loc caselist =
let in_function = if List.length caselist = 1 then in_function else None in
let cases =
List.map2
(fun (pat, _, (ext_env, unpacks)) {pc_lhs; pc_guard; pc_rhs} ->
(fun (pat, _, (ext_env, unpacks)) {pc_lhs = _; pc_guard; pc_rhs} ->

This comment has been minimized.

@garrigue

garrigue Mar 12, 2018

Contributor

Why this change? Is there anything new here?

This comment has been minimized.

@trefis

trefis Mar 12, 2018

Author Contributor

Because contains_gadt is now called on pat and not pc_lhs which is not used anymore.

This comment has been minimized.

@garrigue

garrigue Mar 12, 2018

Contributor

It took me a while to remember that pc_lhs (in this context) is from the pasetree, and pat is from the typed tree...
OK, now I understand the change.

Note that it also means that you could delay building the copied environment to after typing the patterns (since their typing does not depend on values in the environment), and only copy identifiers used in GADT branches.
If this copying is the reason for the slowdown, this would completely remove it.
This could be in particular useful for let-expressions matching on a single-case sum-type.

This comment has been minimized.

@trefis

trefis Mar 12, 2018

Author Contributor

It took me a while to remember that pc_lhs (in this context) is from the pasetree, and pat is from the typed tree...

Sorry, should have made that clearer.

Note that it also means that you could delay building the copied environment to after typing the patterns (since their typing does not depend on values in the environment), and only copy identifiers used in GADT branches.
If this copying is the reason for the slowdown, this would completely remove it.

Yes, I thought about that. But it's not completely clear whether it would be a win or not. At the moment we duplicate all the identifiers appearing in patterns containing a constructor, but we do it only once. Whereas if we did it after having typed the pattern, we would do it only for branches actually containing GADT constructors, but we might have to copy the same identifiers over and over again (because each branch gets its own environment).
It's probably worth a try though; but I'll do it separately from this PR if that's alright.

This comment has been minimized.

@garrigue

garrigue Mar 13, 2018

Contributor

No, you could collect the identifiers from all branches that actually contained gadt patterns, and copy them only once. I.e. basically the same as now, but move it just after the type-checking of patterns (but before calling the pattern_force). There is no need to copy the environment before. Could you give it a try?

This comment has been minimized.

@trefis

trefis Mar 15, 2018

Author Contributor

I think I see what you mean. I'll give it a try sometime in the next few days and report back.

@garrigue

This comment has been minimized.

Copy link
Contributor

garrigue commented Mar 12, 2018

I did approve, as this seems to be a safe change, and simplifies things.
It would be good to have a better analysis of the cost. The copying may not be that big: it is only for identifiers free in branches where an equation might be introduced.

I have a small concern, but not directly related to your change: I'm not 100% sure that this copy has no effect when no equations are introduced. I.e., I tried a backtracking approach, using introduction of equations as criterion, but failed earlier than that. The problem is that we never formalized the relation between scope and levels...

@trefis trefis force-pushed the trefis:disambiguate-gadts branch from af58f13 to 8ef0d3d Mar 12, 2018

@trefis

This comment has been minimized.

Copy link
Contributor Author

trefis commented Mar 12, 2018

I rebased (and squashed all the commits), doing the changes suggested by @gasche in the process.

Changes Outdated
@@ -5,6 +5,9 @@ Working version

### Language features:

- MPR#6023, GPR#1648: Allow type-based selection of GADT constructors
(Thomas Refis, review by Jacques Garrigue and Gabriel Scherer)

This comment has been minimized.

@gasche

gasche Mar 12, 2018

Member

I think Leo could be in here (as a reviewer?) as he did some nice explanation work that was useful for at least my own understanding of your work.

This comment has been minimized.

@trefis

trefis Mar 12, 2018

Author Contributor

Indeed, I've fixed this.

straightforward GADT disambiguation
Also: bootstrap + Changes

@trefis trefis force-pushed the trefis:disambiguate-gadts branch from 8ef0d3d to 15e8f62 Mar 12, 2018

@gasche gasche merged commit e74c1cd into ocaml:trunk Mar 12, 2018

2 checks passed

continuous-integration/appveyor/pr AppVeyor build succeeded
Details
continuous-integration/travis-ci/pr The Travis CI build passed
Details
@garrigue

This comment has been minimized.

Copy link
Contributor

garrigue commented Apr 17, 2018

Any follow-up on making this more efficient (discussion in typecore.ml) ?

@trefis

This comment has been minimized.

Copy link
Contributor Author

trefis commented Apr 17, 2018

Not yet, I haven't had much time for compiler related work recently.
But it is still on my TODO list and I'll hopefully manage to give an update in a couple of weeks.

trefis added a commit that referenced this pull request Apr 25, 2018

Merge pull request #1735 from trefis/delay-type-duplication
Delay type duplication in type_cases (follow up to #1648)
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.