CPS-???? | Approaches to Higher-Order Costing

[kozross]

Something of a follow-up to #1143 . Given that costing higher-order (in fact or in deed) builtins is a concern that goes beyond the specific case described in #1143 , I believe it is worth both describing the status quo, and discussing what would need to improve and how.

I would like @kwxm to chime in on this in particular: I have tried my best to describe things accurately, but I may have missed something.

Rendered

[rphair]

@kozross + @kwxm & other reviewers, FYI — although this may be about a different aspect of "costing" — we noted in an earlier CIP meeting that a recently added (or updated) builtin proposed by @colll78 (#1134) was implemented with a higher-order execution time than would have been possible if all alternatives were included in the CIP (or its update) so that an optimal implementation could be chosen.

The CIP editors aren't able to progress this problem on our own & have just recorded it here for now:

• Plutus CIPs: add implementation estimates + recommendations #1138

We'll keep that issue & this PR as separate as they need to be: although some commenters on this PR may wish to contribute to that issue. Our goal for that issue would be a CIP-0035 update about how to document order-of-magnitude cost estimates as necessary to be beneficial to Plutus implementors (cc @Ryun1 @perturbing).

[colll78]

Particularly interesting to me is limited higher order costing approaches (as opposed to higher order costing which is a whole different beast of vastly higher complexity) I wonder if that warrants a different CPS or CIPs to limited higher order costing can also be proposed under this CPS.

[kozross]

@colll78 - what do you see as the difference between 'limited higher-order costing' and 'higher-order costing'? My CPS is partly a call toward figuring out what limits to higher-order costing exist, as well as informing the community of what those are, and why.

It'd be nice if, as a natural consequence of this, we'd also get costing capabilities up to those limits, of course. These capabilities will be 'limited' in some sense almost by definition. Hence, I'm unsure what you mean.

[colll78]

limited higher order costing refers to the costing of limited higher order builtins, which are higher order builtin function which can only apply compositions of existing builtin functions instead of any arbitrary UPLC code.

ie.

`builtinMap :: (IsBuiltinComposition (a -> b)) => BuiltinList a -> (a -> b) -> BuiltinList b

In the above (a -> b) must be a composition of builtin functions ie. (head . tail . tail . snd . unConstrData)

[kozross]

@colll78 - this is an interesting design space which hadn't occurred to me! One major concern I'd have is that a lot of function arguments to something like 'mapping' operations want matching, which isn't available by means of just builtins, or at least not efficiently. For example, matching on builtin Bool is significantly faster than using IfThenElse, and if you need both head and tail of a known non-empty list, using a one-arm match is better than the combination of HeadList and TailList.

Furthermore, composition can be a bit awkward, unless you mean 'composition' modulo arbitrary permutation of arguments? This is veering fairly close to my suggestion of 'no applications except to builtins', just without matching.

[colll78]

@colll78 - this is an interesting design space which hadn't occurred to me! One major concern I'd have is that a lot of function arguments to something like 'mapping' operations want matching, which isn't available by means of just builtins, or at least not efficiently. For example, matching on builtin Bool is significantly faster than using IfThenElse, and if you need both head and tail of a known non-empty list, using a one-arm match is better than the combination of HeadList and TailList.

Furthermore, composition can be a bit awkward, unless you mean 'composition' modulo arbitrary permutation of arguments? This is veering fairly close to my suggestion of 'no applications except to builtins', just without matching.

It is awkward, but it is also significantly easier to cost, and it allows us to have phased release schedule where we can nail higher-order builtins with real use-case feedback and developer input instead of trying to do it perfectly in one go and missing the mark. I think even limited higher order builtins with no modulo arbitrary permutation of arguments will satisfy the vast majority of possible use-cases, certainly long enough to give us time to handle costing of true higher order built-ins with lots of care. The examples of why this would introduce some inefficiency compared to your proposed higher-order builtins are true but are complete micro-optimizations in the scope of what this would provide, limited higher order builtins would reduce the ex-cost of most common operations by 90%+, and the same with builtin matching would reduce these marginally more at the expense of a significantly longer costing / delivery timeline.

I may be misevaluating the difficulty of costing this variant vs the variant with argument application and matching, and if that is the case then all the merrier, if the scope is feasible for your proposed version, then I'm happy.

[rphair]

@kozross your newer pair of CPS PRs were triaged at the CIP meeting today and the consensus is that @kwxm's first order response, as you have requested, would be a simple condition for this CPS to be declared a candidate (though we could surely consider alternate sources of confirmation). If he or another expert reviewer for this particular subject were to confirm feasibility of defining the problem space in this way, it would certainly be sufficient.

Another note: @kevinhammond said in the meeting he has a strong interest in this subject and has written a few papers on it. I'll try to ping him somehow & invite him to the discussion.

[kevinhammond]

Yes, I'll take a look. I've published a POPL paper for example (that is dealing with very general HOF costing) and designed languages for more restricted settings - @kwxm was part of that project

[kevinhammond]

Restricting to second-order functions might be sufficient? That covers a lot of real-world uses. Also you seem to be mainly interested in builtin HOFs (which can have specific cost models) rather than user-definable functions? That's definitely easier to deal with.

For example

map myfun [1..10]

versus

map map

or

myMap myfun [1..10]

or similar. The work that Martin Hofmann and Steffen Jost did exploited linearity, but the analysis was quite complicated IIRC. It was restricted to a strict setting but that would be OK for UPLC

[kevinhammond]

In terms of the cost model, you would need to reflect the base costs into a cost function, and apply these in the right place. If you are restricting to second order functions, that should be easier.

So

mapArray f

should give a cost model such as

\ a -> length a * cost_f

which could then be applied in a concrete application of mapArray provided the length of the argument is known at compile time. It gets harder if you need to construct the cost model from first principles, e.g.

cost_mapArray = \a -> 1 * cost_f + cost_mapArray (next a) + cost_next

Transforming the latter to the former used to require an external solver in the cost analysis. You might be able to build a simple solver within the cost model instead, or perhaps use type-level operations.

One complication with costing HOFs is that you generally can't tell a-priori whether a higher-order function can be costed. It's necessary to try it and see whether the solver accepts it. Sometimes, counter-intuitively, making a function more complex can make it easier to cost (the function becomes restricted).

[kevinhammond]

Final thoughts: I don't know how the UPLC cost analysis is constructed, but this could well involve a major rewrite, of course, if e.g. there now need to be cost-level lambdas. That could be a fun project. There could also be increases in compile time. I don't know how significant that would be (there's already some metaprogramming in the UPLC compiler, AFAIK, so maybe performance isn't a major issue).

[kozross]

@kevinhammond - thank you for the insights! I agree that a restriction to second-order builtins would allow most of what people would want from 'higher order builtins'. Furthermore, we suggested two restrictions to the kinds of function arguments such a higher-order builtin would accept:

• My writeup suggests forbidding applications of anything that isn't a builtin; and
• @colll78 suggested forbidding anything that isn't an application of a builtin.

I'm not sure if this makes the task easier or more difficult.

Would you be able to give me a link to your paper? It might help if we're on the same page.

[kevinhammond]

There is another approach that might work: defunctionalisation transforms HOFs into first order functions. So you could write a defunctionalising Plutus-Plutus transpiler (or Aiken-Aiken transpiler etc). As long as the first order functions are standard Plutus (Aiken etc), then you don't need a new cost analysis

https://en.wikipedia.org/wiki/Defunctionalization

[kevinhammond]

@kozross Here's the POPL paper, but that really deals with lazy evaluation as well as HOFs. It describes a type-level analysis.

https://dl.acm.org/doi/10.1145/1706299.1706327

This is open access, but the work is technically pretty complex (it took 4-5 years and about 20 failed attempts before we could work it out!). It relies on an external solver (we used one that could handle convex hulls).

This was the paper that deal with higher-order functions in a strict setting, IIRC (might be behind a paywall - let me know if you can't get it easily - there may be a preprint on Arxiv for example).

https://link.springer.com/chapter/10.1007/978-3-642-05089-3_23

This is the paper by Martin Hofmann and Steffen Jost - first order, heap allocation and linear but describes the basic principles quite nicely

https://dl.acm.org/doi/10.1145/640128.604148

[rphair]

@kozross I think this ended up in a stall because were were expecting some broad review like we had in #1150 (leading to its belated confirmation today) but we wouldn't want to discriminate against this CPS just because the subject is more esoteric.

Given that we might have to relax our criteria in that way, I think @kevinhammond's own comments above serve as confirmation that this problem statement is of general interest and usefully formulated; so putting it on the agenda here to confirm it as a numbered CPS if editors & potential reviewers agree: https://hackmd.io/@cip-editors/132

@kozross we would still hope for more participants in the discussion (please tag & invite out of band if you can) and we might also assign a CPS number early if @Ryun1 @perturbing agree before that meeting.

[kozross]

@rphair - I believe I've already tagged and out-of-banded everyone I can. I'd still love to hear from @kwxm, primarily as a lot of the techniques in @kevinhammond's linked papers are quite involved. A sense of 'what would be seen as acceptable by the Plutus Core team' in this context would help future CIPs addressing this problem not get bogged down.

[rphair]

@kozross after over 5 years of trying to gauge what's expected of the CIP process, I believe authors & editors are only expected to show "due diligence" (rather than a tangible result) in getting responses from those considered to be stakeholders. It sounds like that's been done in this case so I would be happy to confirm & then merge this — and recommend this to other editors — in due course (i.e. the next 2 CIP meetings: since a quorum of editors is required for both).