A monoid transformer that allows deleting information from a concatenation of monoidal values.
m is a
Deletable m (intuitively speaking)
adds two distinguished new elements
], such that an
occurrence of [ "deletes" everything from it to the next ]. For
abc[def]gh == abcgh
This is all you really need to know to use
values; to understand the actual implementation, read on.
To properly deal with nesting and associativity we need to be
able to assign meanings to things like
][, and so on. (We
cannot just define, say,
[[ == [, since then
([[)] ==  ==
[() == [id == [.) Formally, elements of
m are triples of the form (r, m, l) representing words
[^l. When combining two triples (r1, m1, l1) and (r2, m2, l2)
there are three cases:
- If l1 == r2 then the [s from the left and ]s from the right exactly cancel, and we are left with (r1, m1 <> m2, l2).
- If l1 < r2 then all of the [s cancel with some of the ]s, but m1 is still inside the remaining ]s and is deleted, yielding (r1 + r2 - l1, m2, l2)
- The remaining case is symmetric with the second.
Inject a value into a
Deletable wrapper. Satisfies the
unDelete . toDeletable === id
A "left bracket", which causes everything between it and the next right bracket to be deleted.