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

typing/typedecl: split and factorize fixpoint computations for variance and immediacy #2152

Merged
merged 8 commits into from Nov 18, 2018

Conversation

Projects
None yet
4 participants
@gasche
Copy link
Member

commented Nov 17, 2018

Many properties of (potentially mutually-recursive) type declarations need to be computed by an iterative fixpoint. The OCaml type-checker currently knows of two, variance of type parameters, and immediacy (the immediate attribute, see documentation).

Currently variance and immediacy are computed in a single fixpoint loop, iterating on both as long as one of them has not reached a stable result. This is a bit wasteful (one of them is going to be recomputed more than necessary), and it also makes the code non-modular and annoying to extend if we want to add new properties (precisely my goal, with a new fixpoint computation for unboxed type declarations).

This PR first splits the single loop into two independent loops, and then it implements a new generic loop (on an abstract notion of "typedecl property" with suitable operations) and ports both variance and immediacy to use this new, more generic framework.

@gasche

This comment has been minimized.

Copy link
Member Author

commented Nov 17, 2018

cc @garrigue, who wrote the original code, #188 the PR that added immediacy, and @Armael, who might be interested.

@gasche gasche force-pushed the gasche:typedecl-split-fixpoints branch from 3c36589 to 7f1ec5c Nov 17, 2018

Show resolved Hide resolved typing/typedecl.ml Outdated
@Armael

This comment has been minimized.

Copy link
Member

commented Nov 18, 2018

I haven't tried to understand in all details what the code is doing, but from a high-level perspective this looks like a nice refactoring.

@gasche gasche force-pushed the gasche:typedecl-split-fixpoints branch from 69795ab to d539c81 Nov 18, 2018

@gasche

This comment has been minimized.

Copy link
Member Author

commented Nov 18, 2018

@Armael no pressure, but I can't tell from your message whether you plan to do an actual review, you plan to not do an actual review, or you don't know yet. (Typical observable outcomes are one of: (1) a merge decision, (2) a request for changes before a merge decision can be made, or (3) an indication that a review will not be conducted (typically by lack of time or expertise) and often a passing of bucket to someone else.)

@Armael

This comment has been minimized.

Copy link
Member

commented Nov 18, 2018

Right, sorry. I'll try to do an actual review in the next few days, unless someone else beats me to it.

@Armael

Armael approved these changes Nov 18, 2018

Copy link
Member

left a comment

I have checked that the new code is equivalent to the old code. I also agree that the refactoring is nicer and more flexible. Hence, I approve the PR; it should be safe to merge it as it is now.

Additionally, I have added a few comments on the code that are mostly nitpicking and you are free to address them or not.

I have a last question: could you explain a bit what is the informal semantics of the required list? With only two instantiations (at the moment), and only one that uses it, I'm having a hard time understanding whether it follows a more general principle or is specific to the variance computation.
Do you have more insight from your work on unboxed annotations?

Show resolved Hide resolved typing/typedecl.ml Outdated
Show resolved Hide resolved typing/typedecl.ml Outdated
@gasche

This comment has been minimized.

Copy link
Member Author

commented Nov 18, 2018

Thanks for the review!

Regarding 'req and required: some properties come with an expression of intent from the user: it's the difference between type 'a t = .. (infer the best variance you can) and type +'a t = ... (infer the best variance, but it should be at least +). required represents this requirement, for each declaration in the declaration list. The previous implement would pass requirements for variance, and check that they are respected by the final solution at the end of the fixpoint loop; this is what the required parameter (of type 'req) and the check : env -> id -> 'prop -> 'req -> unit operation on properties are doing.

Properties for which the implementation doesn't currently have such a notion can use unit as their requirement type. This is the case for immediacies in this PR, which follows the current implementation. In fact, there is a notion of requirement for immediacies (if the attribute is used) that is checked someplace else in the code, so I could consider moving it that here -- at type bool option, I suppose.

I haven't thought yet about how to move our [@unboxed] check on top of this infrastructure (@rlepigre and myself implemented our own fixpoint, and I have yet to rebase on top of this later interface), but I don't think we would use non-unit requirements; there is a global requirement coming from the OCaml runtime, that each type (introduced by a type declaration) must be separable, not a per-declaration requirement that would come from the user.

@gasche gasche force-pushed the gasche:typedecl-split-fixpoints branch from d539c81 to a3d8194 Nov 18, 2018

gasche added some commits Nov 18, 2018

typedecl: split the fixpoint computations for variance and immediacy
This change makes the code simpler and easier to extend. It also
avoids useless computation: the two fixpoints may take a different
number of iterations to converge, and the previous code would compute
both properties as long as one of them hadn't converged.
introduce a generic structure for "type-declaration properties"
Also included are a generic combinator, and a port of the variance
computation to the generic scheme -- without both those things, we
wouldn't know we have the right (internal) interface.
typedecl: remove the location from variance requirements
The location can always be reconstructed from `decl.type_loc`. Note
however that variance-computation functions, in particular
`compute_variance_extension` and its callee (`compute_variance_gadt`,
etc.) need to be passed both the requirement and the location, despite
the fact that they also take a `decl` parameter: there are other
use-cases where the location is not the location of the type
declaration -- when processing an extension to an existing type
declaration.

@gasche gasche force-pushed the gasche:typedecl-split-fixpoints branch from a3d8194 to 7b29c55 Nov 18, 2018

@Armael

This comment has been minimized.

Copy link
Member

commented Nov 18, 2018

LGTM. Can merge when CI passes.

@Armael Armael merged commit de99636 into ocaml:trunk Nov 18, 2018

2 checks passed

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

This comment has been minimized.

Copy link
Member

commented Nov 19, 2018

it's the difference between type 'a t = .. (infer the best variance you can) and type +'a t = ... (infer the best variance, but it should be at least +).

I think that's how it should work. But at the moment adding + annotations to GADT-style definitions can actually change the variance from invariant to covariant.

@garrigue

This comment has been minimized.

Copy link
Contributor

commented Nov 20, 2018

Indeed, inference mode is limited to the most simple case: variable type parameter in a public type definition, that does not appear in a constraint, directly or via one of the GADT cases. Otherwise the annotation is required to get any form of variance. The reason is that we need to know the variance of constrained parameters in other to infer that of the variables that appear in them (i.e. we only infer the variance for type variables, not type expressions).

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.