[Builtins] Add support for pattern matching builtins #5486
Conversation
…to effectfully/builtins/pattern-matching-builtins
effectfully
added
Do not merge
Builtins
EXPERIMENT
effectfully
force-pushed
the
effectfully/builtins/pattern-matching-builtins
branch
from
97f7e94
to
dfdd042
Compare
|
I'm a bit confused about what this would entail for the PLC language. |
No new language constructs. New built-in functions ( |
|
I saw the PR, but it's about code and I don't fully understand the consequences of the code for PLC. What would be the type of |
| (\(u : unit) -> z) | ||
| (\(u : unit) -> f (headList {a} x) (tailList {a} x)) | ||
| (\(x : a) (xs' : list a) (u : unit) -> f x xs') |
There was a problem hiding this comment.
If i understand correctly, we would need to allow higher-order builtins?
There was a problem hiding this comment.
That is, is caseList : all a b. list a -> (unit -> b) -> (a -> list a -> unit -> b) ?
Why is the unit in the last argument needed?
There was a problem hiding this comment.
If i understand correctly, we would need to allow higher-order builtins?
Yes, but only in the metatheory, the implementation supports arbitrary Plutus types in type signatures of builtins (i.e. the metatheory does it better).
is
caseList : all a b. list a -> (unit -> b) -> (a -> list a -> unit -> b)?
No, the type of caseList doesn't have any units, even though they're used inside. They probably shouldn't be used inside, like with the caseData definition discussion below. Note that this is the nonsensical stuff from the stdlib, so don't think too hard about it, the actual builtin (confusingly named the same) is defined elsewhere, here it's only tested.
| (\(i : integer) (ds : list data) (u : unit) -> fConstr i ds) | ||
| (\(es : list (pair data data)) (u : unit) -> fMap es) | ||
| (\(ds : list data) (u : unit) -> fList ds) | ||
| (\(i : integer) (u : unit) -> fI i) | ||
| (\(b : bytestring) (u : unit) -> fB b) |
There was a problem hiding this comment.
I don't understand why the units are needed if computation is already under a function type.
There was a problem hiding this comment.
Right, I think I just mechanically updated the previous definition which was in terms of chooseData where units were needed without realizing that they're no longer needed. Thank you, will fix.
There was a problem hiding this comment.
In fact, we don't need anything more complicated than
-- | Pattern matching over 'Data' inside PLC.
--
-- > \(d : data) -> /\(r :: *) -> caseData {r} d
caseData :: TermLike term TyName Name DefaultUni DefaultFun => term ()
caseData = runQuote $ do
r <- freshTyName "r"
d <- freshName "d"
return
. lamAbs () d dataTy
. tyAbs () r (Type ())
. apply () (tyInst () (builtin () CaseData) $ TyVar () r)
$ var () d| toBuiltinMeaning _ver CaseList = | ||
| makeBuiltinMeaning | ||
| caseListPlc | ||
| (\_ _ _ _ -> ExBudgetLast mempty) -- TODO. |
There was a problem hiding this comment.
I was wondering what happens to the cost...
There was a problem hiding this comment.
We always do a constant amount of work, so should be constant and not very hard to measure. One part that may be tricky is distinguishing (costing-wise) between returning a function application from a builtin and evaluating that application in the CEK machine. But we probably can adapt the current Kenneth's trick of using dedicated no-op builtins. Anyways, we should only discuss it if we think pattern matching builtins make sense, otherwise we'll just waste a bunch of time. I do believe costing shouldn't be an issue, but I might be wrong about that.
There was a problem hiding this comment.
That's good to know. I assumed so, but when I asked why there is no higher-order builtin (especially for cases like the ones here where higher-order is the most natural formulation) I was told that it was because of the costs, so I was wondering if there is any problem here.
There was a problem hiding this comment.
That's good to know. I assumed so, but when I asked why there is no higher-order builtin (especially for cases like the ones here where higher-order is the most natural formulation) I was told that it was because of the costs
We can define higher-order builtins already and we can cost the definable ones properly. E.g. \(f : integer -> integer) -> f is a higher-order builtin, but it's definable and is clearly constant-cost, so there's nothing fancy about costing it.
I think the person giving you comments on higher-order builtins was likely thinking about applying functions and actually reducing them from within a builtin, which we do not support indeed, but
- we did support that in the past
- we'd never costed that functionality, but given that it was simply continuing evaluation before returning from the builtin using the same evaluator without any state reinitialization or discarding, I don't think there were any costing issues either, it just didn't matter if the CEK machine (or any other evaluator) execution was invoked directly or continued from within a builtin
so I was wondering if there is any problem here.
Anyhow, take my words with a grain of salt, I might be failing to spot an issue with costing pattern matching builtins.
It's in the PR, the or if you're not a Cylon: This is the type of the built-in function, i.e. what this PR proposed to implement support for. We also have a function that is confusingly named the same (the one in |
I think types aren't complicated? You just add Specifying the operational semantics of builtins does sound somewhat complicated. "So if Which is why my original plan was to allow arbitrary trees of application (in the sense of |
Is the "real" answer here that we can return any term that introduces no new variable binders? e.g. introducing Of course, our arguments are values and not terms, so we can't actually construct a term, instead we have to construct an evaluation continuation or something, so that does make things more complicated. And maybe the most useful and straightforward evaluation continuation is just a spine of applications. Although even then... can I do this? or this? |
…to effectfully/builtins/pattern-matching-builtins
effectfully
force-pushed
the
effectfully/builtins/pattern-matching-builtins
branch
from
dc78710
to
a551cb4
Compare
…to effectfully/builtins/pattern-matching-builtins
|
/benchmark plutus-benchmark:nofib |
|
Click here to check the status of your benchmark. |
|
/benchmark plutus-benchmark:lists |
|
Comparing benchmark results of 'plutus-benchmark:nofib' on '159e5bd8e' (base) and '26b546339' (PR) Results table
|
|
Click here to check the status of your benchmark. |
|
+3% on average on the builtins-heavy |
|
Comparing benchmark results of 'plutus-benchmark:lists' on '159e5bd8e' (base) and '26b546339' (PR) Results table
|
|
@michaelpj seems like I forgot to hit "comment" last time I wrote a response to your latest comment. Here's another attempt.
Yeah, I guess, although we don't seem to need Although we could allow constructing arbitrary terms as long as it's impossible to embed values supplied as arguments into them, so that there's no chance of mixing up original and created-by-the-builtin variables, but I'm not even sure what we could use that for, so probably not worth discussing it.
Yep, the machinery implemented in this PR is enough for that, just checked: this :: Opaque val (Integer -> a -> b) -> Opaque val a -> Opaque (HeadSpine val) b
this h (Opaque a) = headSpine h [fromValue (1 :: Integer), a]
Not with the machinery implemented in this PR (neither nested application nor builtin calls are supported within the denotation of a builtin), but we can add support for those later if we want to. |
|
Comparing benchmark results of 'lists' on '4b8e137e1' (base) and '490183b6c' (PR) Results table
|
…to effectfully/builtins/pattern-matching-builtins
effectfully
removed
the
EXPERIMENT
…to effectfully/builtins/pattern-matching-builtins
…to effectfully/builtins/pattern-matching-builtins
…to effectfully/builtins/pattern-matching-builtins
effectfully
temporarily deployed
to
github-pages
GitHub Actions
Inactive
effectfully
temporarily deployed
to
github-pages
GitHub Actions
Inactive
plutus-benchmark/marlowe/test/semantics/9.6/semantics.size.golden
Outdated
Show resolved
Hide resolved
...ore/plutus-core/test/TypeSynthesis/Golden/Signatures/ExtensionFun/ScottToMetaUnit.sig.golden
Show resolved
Hide resolved
plutus-tx-plugin/test/size/Golden/Rational/Serialization/fromBuiltinData.size.golden
Show resolved
Hide resolved
plutus-core/untyped-plutus-core/src/UntypedPlutusCore/Transform/CaseOfCase.hs
Show resolved
Hide resolved
…to effectfully/builtins/pattern-matching-builtins
effectfully
temporarily deployed
to
github-pages
GitHub Actions
Inactive
effectfully
temporarily deployed
to
github-pages
GitHub Actions
Inactive
|
Closing in favor of #6530. |
The main change is replacing
with
where
HeadSpineis a fancy way of sayingNonEmpty:(we define a separate type, because we want strictness, and you don't see any bangs, because it's in a module with
StrictDataenabled).The idea is that a builtin application can return a function applied to a bunch of arguments, which is exactly what we need to be able to express
caseListas a builtin:
Being able to express [1] (representing
z) and [2] (representingf x xs) is precisely what this PR enables.Adding support for the new functionality to the CEK machine is trivial. All we need is a way to push a
Spineof arguments onto the context:and a
HeadSpineversion ofreturnCek:Then replacing
with
(and similarly for
BuiltinSuccessWithLogs) will do the trick.We used to define
caseListin terms ofIfThenElse,NullListand eitherHeadListorTailListdepending on the result ofNullList, i.e. three builtin calls in the worst and in the best case. Then we introducedChooseList, which replaced bothIfThenElseandNullListincaseListthus bringing total amount of builtin calls down to 2 in all cases. This turned out to have a substantial impact on performance. This PR allows us to bring total number of builtin calls percaseListinvokation down to 1 -- theCaseListbuiltin itself.