Conversation
|
Can you elaborate why |
treeowl
force-pushed
the
deprecate-seqSpine
branch
2 times, most recently
from
47592dc to
e17bdd5
Compare
Exactly. I've updated the documentation to explain that, and I've also added references to more functions with similar issues in he |
The `seqSpine` function was useful back in the day when all sorts of operations were written in a way that allowed thunks to accumulate along the spine. Now, we carefully force as much of the spine as the amortized bounds allow, which eliminates this problem in general. The only operations that still accumulate thunks along the spine are monotonic maps, and forcing the spines of those just leads to the creation of more thunks at the leaves—it's not really useful.
treeowl
force-pushed
the
deprecate-seqSpine
branch
from
e17bdd5 to
e3c2b96
Compare
|
Mapping over a queue gives you (a thunk for) the first element, and a thunk for the rest of the queue. As you push your way down the spine, successive vertebrae each produce larger and larger numbers of thunks. |
| -- | \(O(\log n)\). @seqSpine q r@ forces the spine of @q@ and returns @r@. | ||
| -- | ||
| -- Note: The spine of a 'MaxPQueue' is stored somewhat lazily. Most operations | ||
| -- Note: The spine of a 'MinPQueue' is stored somewhat lazily. Most operations |
There was a problem hiding this comment.
This was correct, wasn't it?
|
Hahaha. This entire PR is based on me getting confused. Whooops. There really was a (minor) reason for these functions to persist, and it actually was only the functions that were in the documentation. I should explain more about why that is somewhere... |
2 participants
The
seqSpinefunction was useful back in the day when all sorts of operations were written in a way that allowed thunks to accumulate along the spine. Now, we carefully force as much of the spine as the amortized bounds allow, which eliminates this problem in general. The only operations that still accumulate thunks along the spine are monotonic maps, and forcing the spines of those just leads to the creation of more thunks at the leaves—it's not really useful.