Conversation
mheinzel
force-pushed
the
mheinzel/prototype-tests-nested-union
branch
from
83f94db to
9e43f0e
Compare
mheinzel
force-pushed
the
mheinzel/prototype-empty-levels
branch
from
6cdeda2 to
f90b172
Compare
jorisdral
left a comment
jorisdral
left a comment
There was a problem hiding this comment.
This is a useful change 😄
We talked over other channels about this PR, so 'm just leaving some comments to keep track of what we talked about
We also considered how empty levels would influence the implementation, in particular backwards compatibility for snapshots, and we agreed that it's probably going to be straightforward to support backwards compatibility. We're roughly going from a levels structure analogous to [NonEmpty Run] to a structure analogous to [Maybe (NonEmpty Run)], and the former maps easily into the latter
| data IncomingRun s = Merging !MergePolicyForLevel | ||
| !NominalDebt !(STRef s NominalCredit) | ||
| !(MergingRun LevelMergeType s) | ||
| | Single !Run |
There was a problem hiding this comment.
We talked about keeping Single, but I'm just leaving a summary of my thoughts on it here for posterity:
I'd argue in favour of keeping Single to encode invariants statically, because we are now replacing that with extra assertions in levelsInvariant & co. In my mind it's analogous to using NonEmpty over [] when you know a list should be non-empty (though the prototype is obviously more complex and therefore the choice of representation is a more nuanced tradeoff). Yes, there are more case-expressions you need to write in levelsInvariant, but being forced to be explicit about these cases is in my mind clearer and less error-prone.
| -- to see statically that it's a single run without having to read the 'STRef', | ||
| -- and secondly to make it easier to avoid supplying merge credits. It's not | ||
| -- essential, but simplifies things somewhat. | ||
| data Level s = Level !(Maybe (IncomingRun s)) ![Run] |
There was a problem hiding this comment.
I think we agreed we would try out a representation where the level can be either empty, or non-empty. Something along the lines of
data Level = EmptyLevel | Level ...There was a problem hiding this comment.
Done now. We still need to merge #814 first and rebase, so I'll leave it as a draft PR for now. But apart from that, this branch should be ready.
mheinzel
force-pushed
the
mheinzel/prototype-tests-nested-union
branch
from
9e43f0e to
b7bc5c2
Compare
It makes more sense for it to take PreExistingRuns directly, instead of first turning each level into IncomingRuns and then turning those into PreExistingRuns.
mheinzel
force-pushed
the
mheinzel/prototype-empty-levels
branch
from
f90b172 to
2591aff
Compare
| levelsInvariant !_ (EmptyLevel : ls) = do | ||
| assertST $ not (null ls) -- last level shouldn't be empty |
There was a problem hiding this comment.
👍 makes sense, we don't want "trailing empty levels" so to speak
|
|
||
| go !ln incoming (EmptyLevel : ls) = do | ||
| let mergePolicy = mergePolicyForLevel ln [] ul | ||
| traceWith tr' $ LevelIsNotFullEvent mergePolicy |
There was a problem hiding this comment.
Minor: it might nice to have a separate trace constructor for this
| tr' = contramap (EventAt sc ln) tr | ||
|
|
||
| go !ln incoming (EmptyLevel : ls) = do | ||
| let mergePolicy = mergePolicyForLevel ln [] ul |
There was a problem hiding this comment.
I think this should take into account later levels, no?
| let mergePolicy = mergePolicyForLevel ln [] ul | |
| let mergePolicy = mergePolicyForLevel ln ls ul |
2 participants
Builds on top of #814.
This can generally be useful, but the main motivation now is to allow migration of the union level into the regular levels as soon as the merging tree is completed.
So far, we always required an
IncomingRunto be present on each level, but already had a special case for where this could be a plainRunthat doesn't require any merging. Instead, we can make the presence of theIncomingRunitself optional, which allows us to have no runs on a level at all. The resulting changes are minor, but we should perhaps think about more suitable terms forIncomingRunand/or theMaybe IncomingRun(which might deserve its own data type), at least in the real implementation).