CIP-0194? | Plutus Core builtin matchDataConstr - #1236
Conversation
rphair
left a comment
There was a problem hiding this comment.
@SeungheonOh thanks very much for documenting your implementation with a CIP. The in-progress work I think makes it definite we would assign a CIP number in Triage at the next CIP meeting (https://hackmd.io/@cip-editors/140).
@zliu41 @ana-pantilie @colll78 @Quantumplation @fallen-icarus if you could review the CIP technical presentation any time before or after its confirmation, that would be great.
@kwxm it looks like performance is already also well documented here, but please likewise feel free to contribute about that presentation as well.
|
Strongly support this CIP, approach is sound and a massive improvement. |
|
|
||
| ### Costing | ||
|
|
||
| All work performed by `Match` is charged incrementally. Matching steps are divided into four CEK step kinds: |
There was a problem hiding this comment.
This is rather different to how costing works for other terms, where a cost is associated with the reduction rule for a term.
Here we either have one very big reduction rule, or we would need a way to evaluate the match incrementally. But the possibility of backtracking in the matching makes this difficult.
There was a problem hiding this comment.
As implemented, latter is the case. Match is being costed incrementally. Backtracking doesn't really pose any issue since it also increments the costs for failed cases, so it doesn't have to do anything complicated for failed branches.
I wrote this in a confusing way. Not all four steps being proposed are CEK steps. Only one is for CEK itself, and other three are steps used within the matcher.
There was a problem hiding this comment.
Backtracking doesn't really pose any issue since it also increments the costs for failed cases, so it doesn't have to do anything complicated for failed branches.
Backtracking makes it harder to give an incremental reduction behaviour. Perhaps we still could - if we eliminate a branch then we can remove it from the match.
|
|
||
| ### Evaluation | ||
|
|
||
| `Match` is evaluated as follows: |
There was a problem hiding this comment.
I would like to see a more declarative and less operational description of how this works. Typically we give a reduction rule for terms.
| | DefaultPatternFieldsPrefixWildcard | ||
| | DefaultPatternFieldsPrefixCapture | ||
|
|
||
| data DefaultBuiltinPattern |
There was a problem hiding this comment.
This is a lot of syntax. Probably this increases the size of the base language by 30%+!
| 2. If the result is not a builtin constant, evaluation fails. Otherwise, inspect alternatives in source order. | ||
| 3. Match an alternative depth-first, from left to right, recording captures as they are reached. | ||
| 4. On a mismatch, discard that alternative's pending work and captures, then try the next alternative. | ||
| 5. On success, select that alternative's handler and apply the captured values to it in source order. |
There was a problem hiding this comment.
Are the handlers evaluated strictly before evaluating the match?
There was a problem hiding this comment.
No, none but the matching handler will be evaluated. Only patterns that comes before the matching case will be inspected.
I'll try to clarify this section
For example:
(match (con integer 2)
(pattern (integer 0) (error)) -- Pattern inspected, but not evaluated
(pattern (integer 1) <expensive work>) -- Pattern inspected, but not costed/evaluated
(pattern (integer 2) (con integer 42))
(pattern (integer 3) (error)))
-- > (con integer 42)
There was a problem hiding this comment.
That seems fine, it mirrors case.
|
|
||
| #### A dedicated `Let` term | ||
|
|
||
| A `Let` term could bind a row of values but still requires CEK support for that row and overlaps with lambda/application as a binding mechanism. Like multi-lambda, it does not provide general nested matching. |
There was a problem hiding this comment.
yes, this seems orthogonal
|
|
||
| The following local benchmarks compare `Match` with existing deconstruction using partial builtins, optionally guarded by `chooseData`, or builtin `Case`. They measure CEK wall-clock time rather than calibrated on-chain execution units. | ||
|
|
||
| #### Capturing one deeply positioned value |
There was a problem hiding this comment.
So... why is this faster? Operationally speaking. We are fundamentally doing a very similar process. Is it just that we skip some expensive parts of the builtin machinery? It seems odd that we're able to do the same thing but faster!
There was a problem hiding this comment.
It's mainly the builtin calling overhead. Calling builtin requires several extra CEK frames. In most cases, it needs Apply and Builtin and for some it also requires extra Forces. These need to happen per each layer of nested values and these overheads turns out to be more expensive than actually deconstructing values themselves.
Match removes all of the overhead only running on very lean pattern syntax and doing value deconstruction directly removing significant amount of the overhead. This is exactly the same reason why IfThenElse is slower(almost 80% iirc!) than Case when casing on boolean.
Also, Match gives options to match pattern without capturing value, this reduces CEK steps even more. For instance, if you just want to check if D.I 10 is integer data or not, currently, you'd do chooseData (D.I 10) ... (\i -> ...) ... where builtin not only have to match on the Data constructors, but it also have to capture 10 and apply to the handler even though the value is not needed. This also incurs more extraneous cost. Match on the other hand can do (pattern (data-i (wildcard) <arity 0>) which doesn't have to dispatch apply at all. This is why the performance gap is bigger when fewer captures were performed in the benchmarks
There was a problem hiding this comment.
Well, we still need to do the work of evaluating arguments and applying them to functions. Are we just not book-keeping that on the stack?
There was a problem hiding this comment.
If doing it all in one go is what helps, then maybe we really do need to compare this to multi-lambdas and multi-application.
| `Match` is evaluated as follows: | ||
|
|
||
| 1. Evaluate the scrutinee. | ||
| 2. If the result is not a builtin constant, evaluation fails. Otherwise, inspect alternatives in source order. |
There was a problem hiding this comment.
Should we allow matching on other values? Notably, what about con values? If we're going to add pattern-matching it's a shame not to get it on datatype values.
There was a problem hiding this comment.
Do you mean Constrs? I didn't add it because I initially thought it could break typing in TLPC/PIR. However, looking again, it seems reasonable to add something like DefaultPatternConstr Word64 (Vector DefaultBuiltinPattern).
I'm not entirely sure performance implication to adding this. This would definitely complicate the implementation(which can consequently make it slower) because having pattern for Term.Constr means now it needs to carry and match on Term not just values.
There was a problem hiding this comment.
Constrs are a kind of value, though?
| | DefaultPatternByteString !ByteString | ||
| | DefaultPatternBool !Bool | ||
| | DefaultPatternUnit | ||
| | DefaultPatternList |
There was a problem hiding this comment.
Why not?
DefaultPatternList { headPattern :: DefaultBuiltinPattern, tailPattern :: DefaultBuiltinPattern }
you'd need DefaultPatternNil, perhaps, to terminate them. But I'm a bit unsure about using this prefix/exact shape descriptor rather than a pattern AST that follows the shape of the datatypes.
There was a problem hiding this comment.
This would make pattern interpretation slower since for matching long list, it would need to match on DefaultPatternList repeatedly. I figure it's better to prefer structure that is more optimal to run since this won't be user facing interface anyways.
|
The structure is odd compared to the usual pattern matching. Your form: (match scrutinee (pattern pair (pair (bind) (bind)) (bind))) (lam x (lam y (lam z body)))) Usual form: (match scrutinee (pattern pair (pair x y) z)) body) In both cases, the body refers to x, y, z as bound variables. The first form reuses the existing lambda machinery, while the second does not, so I guess the first is slightly easier to implement. But nowhere is the usual form mentioned or compared with. I think there is good reason to believe that the second can be implemented more efficiently (although it may take more work to do so). So a comparison is essential. Typically, a compiler gets rid of nested pattern matching and only uses a shallow case to look at the top-level structure. Your motivation is that the existing mechanism which does this can (if misused) lead to partial applications, but an easier way to fix that is to supply an arity with each case rather than nested pattern matching. Did you compare with that alternative? You need to add this comparison the the CEP to justify the design. Michael noted that for lists matching on cons and nil instead of prefix is standard. Sungheon responded that the prefix design is more efficient, which sounds plausible. But this needs to be documented with performance numbers in the CEP. If match is included it should also apply to sum-of-product types. (I think Michael makes a similar point.) |
rphair
left a comment
There was a problem hiding this comment.
@SeungheonOh this was declared a candidate at the CIP meeting today, continuing the prior confirmations. Going forward we will generally await the settlement of current & future review like what @michaelpj has already provided (please "resolve" the points that seem to be settled, since this might not always be clear to editors).
Once generally settled please feel free to explicitly point this out in a comment, so we can make sure it moves on to final / editorial review. In the meantime please rename the containing directory to CIP-0194 and update the "Rendered" link in your OP. 🎉
|
Thank you, @wadler and @michaelpj, for the review! About binding captures directlyIt seems that a similar design was considered when SOP terms were added in CIP-85, but was ultimately not adopted. CIP-85 mentions that this optimization initially produced an improvement of around 10%. However, another optimization reduced the realized improvement from direct binding to only around 3%, which was considered a small enough difference to justify preferring the simpler implementation. I am not sure exactly what that other optimization was, or whether there were additional reasons for not using direct binding in CIP-85. Maybe @michaelpj can provide more context here. I tested direct binding for About (re)using
|
zliu41
left a comment
There was a problem hiding this comment.
I need to review it in more detail, but here are some initial comments:
- It's worth elaborating why "A handler with the wrong number of arguments may therefore partially apply instead of failing" is problematic
- The baseline in your benchmark should use the new
dropListbuiltin, if not already - It would be interesting to know how much this approach narrows the performance gap between Data encoding and SOP encoding. Can it close the gap entirely? If not, why?
|
Regarding the long list of patterns, I'd suggest shortening them as much as you can.
|
|
What is the reason behind delegating variable binding to the handler instead of using a matching mechanism which constructs substitution contexts? Concretely, if I understand this correctly, in the following example:
However, if Then it would be up to the matching algorithm to produce a valid substitution for I think it would also make matching more expressive: After beta-reduction, the matching algorithm would not be able to find a valid substitution for Of course, my suggestion would require a more complex costing mechanism to account for the substitution construction. But I think that using a proper matching algorithm would make it more future proof, in case we want to add new features to |
|
|
||
| where $M$ is the scrutinee, $p_i$ is a universe-specific builtin pattern, and $H_i$ is its handler. The alternatives are ordered. | ||
|
|
||
| A builtin constant is written $C=\langle u,v\rangle$, pairing a universe tag $u$ with a value $v:\mathsf{El}(u)$. The UPLC constant term containing $C$ is written $\ulcorner C\urcorner$. A capture sequence is written $\overline C=[C_1,\ldots,C_k]$, and $\epsilon$ is the empty sequence. Sequence concatenation is $\mathbin{+\!+}$. |
There was a problem hiding this comment.
You would be far ahead of me in LaTeX maths but I understand this expression will simply render the argument of \mathbin in a typeface consistent with other math. It therefore is doing what I would expect it to do: what were you intending?
A previewer shows the same thing, with a little difference in horizontal spacing: https://quicklatex.com
There was a problem hiding this comment.
In LaTeX the \! represents a small negative space, moving the two +s closer together. I think this is suppose to render as ++, maybe with no space in the middle.
I have no idea how to fix it though. Markdown renderers seem to be a bit inconsistent.
There was a problem hiding this comment.
thanks; I don't know why I thought a literal ! was coming out in the markup from the previewer before... I can't see it there now. Indeed it looks there like the + signs are conjoined and I can see now what you were getting at. Maybe:
- some more of these maths presentation issues would be documented on https://github.com/github/markup/issues like the one below (or you could ask there);
- I can do a quick poll at the CIP meeting to see if any maths formatting enthusiasts have anything to suggest.
|
|
||
| the matching function returns | ||
|
|
||
| $$ |
There was a problem hiding this comment.
This renders properly on that previewer
... so at least one thing is working differently here on GitHub. @michaelpj what do you think?
There was a problem hiding this comment.
p.s. @kwxm maybe escaping the # character will fix it on GitHub?
|
|
||
| ### Backward compatibility | ||
|
|
||
| The change is backward-compatible at the Plutus Core language level because `Match` is guarded by a new minor language version. Scripts using earlier versions continue to parse and evaluate with unchanged semantics. |
There was a problem hiding this comment.
Bear in mind that data will probably be getting an extra value constructor [in Plutus V4](https://github.com/zliu41/CIPs/blob/v4/CIP-0195/README.md#list-vs-array.. I think we can make that backward compatible with the current version of data using a semantic variant. Presumably the stuff described in this CIP would need to be extended to work with the new version, and only the new version. Would that cause any extra difficulty?
|
I explored achieving similar matching performance with a builtin function instead of introducing a dedicated Match AST node, and the builtin appears to be the better direction. The builtin design also moves most of the static complexity into PLC. PLC validates the matching description and determines its result SOP type. After erasure, UPLC receives an ordinary ByteString and evaluates it through the existing builtin machinery, returning a VConstr for dispatch by Case. This preserves structural erasure and avoids adding new pattern or binding machinery to UPLC. The current costing parameter for the builtin and |
|
@rphair I made big changes that basically removes most content from the original proposal in favor of new approach. I wasn't sure if it needed a new CIP PR or not so I just updated this one. The changes are still on topic of making |
There was a problem hiding this comment.
(@SeungheonOh I'm editing my comments in here since my last review crossed your own last posting above)
The scope of this CIP is still to achieve what was originally imagined & we see many cases like that over the course of a CIP PR lifetime. So there is absolutely no necessity (and, I believe, no advantage) in requiring a new PR for this. 😎
4f6d9c8 to
ff08f20
Compare
ff08f20 to
2b74da3
Compare
Co-authored-by: Robert Phair <rphair@cosd.com>
359016a to
c8a02f0
Compare
matchDataConstr
|
We've implemented IntersectMBO/plutus#7914 which is related to this CIP. This PRs adds casing As this change uses existing casing mechanism and doesn't add any new mechanism, it is completely independent of different ideas proposed in this CIP. |

Proposal for adding a new UPLC AST node:
Match.Matchenables matching complex and nested builtin value structure, namelyDatavalues like script context, without builtin function invocation overhead.A working prototype has been implemented: IntersectMBO/plutus#7852
Rendered