Restructure modal and with-bounds (fka baggage) in jkind #3457
+858
−962
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
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.
glittershark
added
the
modes
glittershark
commented
Jan 9, 2025
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
[CI] Use setup-ocaml v3 for ocamlformat workflow
glittershark
changed the title
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.