Faithfully print with-kinds by reconstructing modalities for types #3410
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
force-pushed
the
aspsmith/normalize-mode-axis-types
branch
from
4c2935f to
f2abf37
Compare
glittershark
force-pushed
the
aspsmith/untype-jkind
branch
from
ca413c7 to
9a621e1
Compare
glittershark
force-pushed
the
aspsmith/normalize-mode-axis-types
branch
from
f2abf37 to
3b9194f
Compare
glittershark
force-pushed
the
aspsmith/untype-jkind
branch
from
9a621e1 to
6aaacea
Compare
glittershark
force-pushed
the
aspsmith/normalize-mode-axis-types
branch
from
3b9194f to
cb9f1f9
Compare
glittershark
force-pushed
the
aspsmith/untype-jkind
branch
from
6aaacea to
cb56621
Compare
glittershark
force-pushed
the
aspsmith/normalize-mode-axis-types
branch
from
cb9f1f9 to
7f571bb
Compare
glittershark
force-pushed
the
aspsmith/untype-jkind
branch
from
cb56621 to
7699e54
Compare
glittershark
force-pushed
the
aspsmith/normalize-mode-axis-types
branch
from
7f571bb to
e8ad948
Compare
glittershark
force-pushed
the
aspsmith/untype-jkind
branch
4 times, most recently
from
1d38927 to
c1b370e
Compare
glittershark
changed the title
|
not quite sure what's going on with the test failure here; hopefully this is reviewable regardless? |
glittershark
force-pushed
the
aspsmith/normalize-mode-axis-types
branch
from
e8ad948 to
ffeb5de
Compare
glittershark
force-pushed
the
aspsmith/untype-jkind
branch
from
c1b370e to
c7f5c82
Compare
Per zqian's CR to this effect. note that this does not do any of the simplification that this unlocks yet, that'll happen later
Now that the types for jkind axes and mode axes have been unified, we can express the condition for "modality is const for axis" directly, without resorting to a huge ugly pattern match on the axis and the modality's atoms.
glittershark
force-pushed
the
aspsmith/normalize-mode-axis-types
branch
from
ffeb5de to
6ab8dcd
Compare
glittershark
force-pushed
the
aspsmith/untype-jkind
branch
from
c7f5c82 to
a830b3a
Compare
we need to sort types in a [with] because the order comes from iterating a TypeHash, which is nondeterministic (specifically, the order is different if we disable stack allocation) and brittle. Unfortunately, we lack a good comparison for types, so as a hacky workaround here we format to a string (actually, a string list for easier line breaking when pretty printing) and sort lexicographically before finally printing.
glittershark
force-pushed
the
aspsmith/untype-jkind
branch
from
56f9967 to
5a7d986
Compare
Base automatically changed from
aspsmith/normalize-mode-axis-types
to
aspsmith/with-kind-modalities
January 6, 2025 11:02
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.
Reconstruct a more faithful representation of
with-kinds when constructing outcome jkinds fromJkind.ts, using constant modalities on axes to omit types from axes which don't have those types in their baggage.This approach is pretty dumb (we just walk the baggage of each axis building up a map tracking which types are mentioned on which axes), but from reading the existing test cases it seems to do a pretty good job of constructing the jkind that the user would have written down themselves - plus it's vastly better than the previous approach of just printing a kind that wouldn't even parse, let alone be correct.
Plausibly this approach would need to be rethought completely once we introduce non-constant/identity modalities, but those are far enough off that I claim this should serve us fine for the time being.
Review the whole diff, rather than individual commits.