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 is an experiment regarding array performance. Our current array representation (as essentially a
Rc<[RichTerm]>
) is problematic because it makes many common operations unnecessarily quadratic. This PR replaces it with arpds::Vector<RichTerm>
in reverse order, and the initial benchmarks look promising.In more detail, the current arrays have a few performance characteristics that we might like to keep:
The main problem is that there's no constant-time "cons" operation, and the concatenation operator
xs @ ys
isO(xs.len() + ys.len())
. This makes many functional-style list functions (like the stdlib implementations ofreverse
andfilter
) quadratic in the length of their input.The
Vector
implementation in therpds
crate is a "persistent vector" aka "bitmapped vector trie", which offers persistence/sharing, fast random access, and fast appends. We can do the same slicing trick that we're current using forRc<[RichTerm]>
to also add fast slicing. Thanks to fast appends, we can do concatenationxs @ ys
inO(ys.len())
time (provided that there are no contracts that need to be applied toxs
; I'm also ignoring logarithmic terms). This is backwards from the more common concatenation pattern in functional languages, so we store arrays backwards in order to get timeO(xs.len())
instead. (We could achieve the minimum of the two by storing an array as twoVectors
, a backwards one followed by a forwards one.)There are a few ways in which
rpds::Vector
isn't a perfect fit:Arc
orRc
, which we don't want becauseRichTerm
already has a shared pointerDespite these, this PR gives a 35% improvement in
random normal
, and a few other improvements between 10 and 20%. I'd like to also try benchmarkingim
and/orimbl
.