Restructure modal and with-bounds (fka baggage) in jkind #3457
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
glittershark
added
the
modes
glittershark
commented
Jan 9, 2025
typing/jkind_types.mli
Outdated
Comment on lines
109
to
129
| module With_bounds : sig | ||
| module Type_info : sig | ||
| type +'type_expr t = | ||
| { type_expr : 'type_expr; | ||
| modality : Mode.Modality.Value.Const.t; | ||
| nullability : bool | ||
| } | ||
|
|
||
| val create : | ||
| type_expr:'type_expr -> | ||
| modality:Mode.Modality.Value.Const.t -> | ||
| deep_only:bool -> | ||
| 'type_expr t | ||
| end | ||
|
|
||
| type (+'type_expr, 'd) t = | ||
| | No_baggage : ('type_expr, 'l * 'r) t | ||
| | No_with_bounds : ('type_expr, 'l * 'r) t | ||
| (* There must always be at least one type. *) | ||
| | Baggage : | ||
| 'type_expr * 'type_expr list | ||
| | With_bounds : | ||
| 'type_expr Type_info.t * 'type_expr Type_info.t list | ||
| -> ('type_expr, 'l * Allowance.disallowed) t |
There was a problem hiding this comment.
probably deserves documentation
There was a problem hiding this comment.
The whole idea of with-bounds needs documentation... but given that (user-facing) documentation, this encoding seems straightforward enough.
glittershark
changed the title
glittershark
force-pushed
the
aspsmith/untype-jkind
branch
from
aaa1601 to
1af69a4
Compare
Move the current version of Jkind_axis.Axis_collection, which wraps a type indexed on the specific axis, into `Axis_collection.Indexed`, and make `Axis_collection.t` unindexed. I already have one use case (in printing for jkinds) which doesn't care about the specific axis in the type, and I'm about to introduce another, and this feels like a natural structure.
This commit contains a significant restructuring of the modal upper bounds and with-bounds (which is the new name for what was previously called "baggage") in the innards of Jkind.t Previously, jkinds morally consisted of: - a layout - a map from axis, to a pair of upper bound and a list of types (the with-bounds for that axis) now, we instead have, morally: - a layout - a map from axis to the upper bound for that axis - a list of (type, modality) pairs, where the modality is effectively providing us the way that the type operates on the axis This behavior is both much closer to the syntactic representation of jkinds, making it simpler both to construct and to print, and probably more efficient, since the usual behavior is that a type appears on the with-bounds for all axes (this is only not the case in the presence of modalities) The test changes are mostly innocuous: 1. Printing changed slightly when illegal crossing is used - actually I'm reasonably sure that this change *fixed* printing of kind annotations for types with illegal crossing 2. We're no longer deduplicating types for printing kinds (we used to do this only when constructing outcometrees); this will come back later as we do deduplication of with-bounds at construction time. 3. We actually got better at printing kinds in general, eg we're now better at figuring out built-in aliases to print under some with-bounds. Past the actual internals of with-bounds, we frequently /reconstruct/ the list-of-types-per-axis shape, eg in subsumption - this is mostly done to avoid this commit getting too large and hairy, and in follow-up I plan on refactoring to do more algorithms such as bound extension holistically rather than per-axis, which ought to also realize more performance gains here.
[CI] Use setup-ocaml v3 for ocamlformat workflow
glittershark
force-pushed
the
aspsmith/transpose-jkind
branch
from
5ce9f8b to
6270b24
Compare
goldfirere
reviewed
Jan 15, 2025
|
|
||
| include Allowance.Allow_disallow with type ('a, _, 'd) sided = ('a, 'd) t | ||
| val compose_modality : |
There was a problem hiding this comment.
This strange function can be deleted after we remove illegal crossing.
| match with_bounds1, with_bounds2 with | ||
| | No_with_bounds, No_with_bounds -> | ||
| Axis_ops.less_or_equal bound1 bound2 | ||
| (* CR layouts v2.8: This should expand types on the left. *) |
There was a problem hiding this comment.
Seems like it does now, no?
| let with_bounds1 = | ||
| With_bounds.types_on_axis ~axis sub.jkind.with_bounds | ||
| in | ||
| let modifiers = Axis_ops.equal bound1 bound2 in |
There was a problem hiding this comment.
You can do an le comparison here; equality is not necessary
Co-authored-by: Richard Eisenberg <reisenberg@janestreet.com>
|
I have reviewed the latest four commits ("Apply suggestions from code review"..."remove pointless magic"), with no further comments. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
This commit contains a significant restructuring of the modal upper bounds and with-bounds (which is the new name for what was previously called "baggage") in the innards of
Jkind.tPreviously, jkinds morally consisted of:
for that axis)
now, we instead have, morally:
This behavior is both much closer to the syntactic representation of jkinds, making it simpler both to construct and to print, and probably more efficient, since the usual behavior is that a type appears on the with-bounds for all axes (this is only not the case in the presence of modalities)
The test changes are mostly innocuous:
Past the actual internals of with-bounds, we frequently /reconstruct/ the list-of-types-per-axis shape, eg in subsumption - this is mostly done to avoid this commit getting too large and hairy, and in follow-up I plan on refactoring to do more algorithms such as bound extension holistically rather than per-axis, which ought to also realize more performance gains here.
note for reviewers: the last commit is a cherry-pick from main to get CI passing, and can be ignored. The two other commits can easily be reviewed separately.