Switch to an asymptotically better typing context implementation #6053
Conversation
This file contains hidden or 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
The new representation allows for splitting and rejoining contexts more efficiently. The `Info` type that used to be built up linearly, left-to-right, is now aggregated monoidally (and implicitly) from the elements stored in the tree. The info allows for efficiently splitting contexts at a specific variable (necessary for type checking), and preserves aggregated info in segments. By not discarding this aggregate info, it can just be merged back together when the overall context is rebuilt, which saves linear amounts of work when e.g. solving variables.
This appears to actually be better than the strict fields.
Contributor
|
Awesome, thanks! |
aryairani
approved these changes
Dec 12, 2025
pchiusano
approved these changes
Dec 12, 2025
Member
pchiusano
left a comment
There was a problem hiding this comment.
Very nice. Always great when a fancy data structure actually ends up being useful. :)
I think this is worth a merge and we dogfood it a bit.
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 changes the implementation of the type checking context to be based on finger trees instead of plain lists.
Previously a context was a list of
Elements andInfos, where the latter aggregated information about all the previousElements in the list. This new implementation uses a finger tree ofElements with a modifiedInfotype as the "measure" of the finger tree. EachElementhas a singleton-likeInfomeasure, and the information is aggregated up the tree.This has significant asymptotic advantages in some cases. The
Infomakes it possible to split the context in logarithmic time by looking at which variables are in play in subsequences. Also, by modifying a few parts of the algorithm to operate on these (possibly ill-formed) sequences rather than[Element v loc], the aggregateInfois largely maintained. Previously, the algorithm would often discard the info and recalculate it from the elements when appending to the context, which is linear in the number of elements.Certain pathological type checking examples can result in repeatedly splitting and rejoining large portions of the context. E.G. some tracing of the problem:
indicates that sequences of thousands of elements are repeatedly split off and rejoined from the context. This is actually the majority of the context, so most of it was being rebuilt from scratch. In this patch, the split is more efficient, and quite a bit of aggregate information should be saved, with only a portion from the rejoined context needed to make the large ill-formed portion of the context back into a valid one. Hence, checking this example is now ~10x faster (but the speedup is actually asymptotic (probably something like
n * (log n)^krather than quadratic).The type checking algorithm is overall the same. Just some core pieces where the context is directly manipulated were altered to take advantage of the new structures.
Transcripts seem to pass without change. I'm not sure how comprehensive those are w/r/t type checking changes for something at such a fundamental level. But it's something at least.