CIP-0091? | Don't force Built-In functions

[nielstron]

A rough draft of a CIP that suggests to remove the type instantiations (which are essentially no-ops) from builting UPLC functions.
This should be benefitial for the development of (among others) @aiken-lang, @Hyperion-BT 's helios, and @OpShin 's eopsin.

Rendered draft

[michaelpj]

This CIP is a bit of a sketch, but this is an idea we've considered before and I like it. Well, I like the more extreme version where we just don't let builtins be forced at all.

However, I do think that this is likely to have a relatively minor impact, and so to some degree whether or not we do this depends on how easy it is to implement, particularly in respect to maintaining backwards compatibility (builtins in old language versions must continue to work the same forever!).

[michaelpj]

It's not really more work if we replace them. If it was the case that builtins didn't need to be forced, we could just add an optimization pass that removed all the forces.

[michaelpj]

Sadly, this is true to some degree anyway, since we have to support the old versions forever in the implementation.

[michaelpj]

I would propose a much stronger version of this. Instead of just implementing the current builtins so that they don't require forces, we instead make it so that no builtins ever need forces. That makes the backwards compatibility story trickier for the evaluator, but I think we could manage it.

[michaelpj]

Ideally, I would like to do this in a sneaky way so we can use the same implementation for previous ledger languages as well, but that might be tricky.

[michaelpj]

I would really like an impact assessment of this. My suspicion is that the actual performance impact will be negligible, and the main impact will be on making it easier for compiler writers and simplifying the language. As a compiler writer and a maintainer of the language, I appreciate those things, but they're much weaker reasons than widespread performance improvements IMO.

[effectfully]

I would really like an impact assessment of this.

There was one data point here.

[mjaskelioff]

Also there is a proposed solution there: add the necessary delays before the builtin and let simplification erase the force/delay pairs. One limitation mentioned there was that type arguments are not required to come first, but this can be made a requirement (as we've been discussing elsewhere).

[michaelpj]

It's a non-backwards-compatible change, so it will require a new Plutus ledger language, see CIP-35.

[mjaskelioff]

Would it be non-backwards-compatible if unrestricted force is implemented?

[rphair]

This statement looks like it was finished "... IOG and will thus need their approval." as currently written oin the initial comment for this PR. You are on the right track with @michaelpj's review especially the reference to CIP-0035 which explains the things that would need to go into the Plan to Active.

Since @michaelpj just submitted a CIP also dealing with types in Plutus you can probably just adapt the one here, modifying the section about "benchmarks" to reflect his comments above about performance impact (?): https://github.com/michaelpj/CIPs/blob/mpj/sums-of-products/CIP-%3F%3F%3F%3F/README.md#path-to-active

[L-as]

Don't allow forcing what is necessarily in WHNF.

[effectfully]

What if we simply implement an optimization that binds force (force (builtin fstPair)) to a variable and replaces all occurrences of this expression with that name? And similarly for all other builtins. Then we'll get a constant and pretty negligible amount of overhead per builtin.

While I certainly like the idea of untangling UPLC from TPLC/PIR/Plutus Tx, I'm not sure I like the idea of untangling UPLC from any kind of types. Built-in functions have signatures, those signatures have quantifiers, we should account for quantifiers somehow and force is a sensible way of doing that, semantics-wise. If we can get away with having minimal runtime/size overhead by pulling those forces out of the program, then I'll vote for not weirdifying the language. Particularly because such a change would be even trickier in the blockchain context where we have to maintain backwards compatibility or perform weird and potentially risky tricks.

Inviting @mjaskelioff and @jmchapman to participate in this discussion.

[effectfully]

I would really like an impact assessment of this.

There was one data point here.

[nielstron]

@effectfully What you describe is more or less exactly what i.e. plutonomy does.
I agree its a viable workaround for now and I am fine with it being the eventual outcome.

I am describing here the ideal situation from a user perspective, not from a blockchain developer perspective. Whether or not it is feasible/worthwile is up to discussion.

[michaelpj]

Another data point is here: IntersectMBO/plutus#5112

That suggested that getting rid of a significant fraction of the redundant forces in a program had minimal effect on runtime.

[L-as]

What if we simply implement an optimization that binds force (force (builtin fstPair)) to a variable and replaces all occurrences of this expression with that name? And similarly for all other builtins. Then we'll get a constant and pretty negligible amount of overhead per builtin.

Plutarch already does this. It's not always worth it though, because let-bindings are expensive too.

While I certainly like the idea of untangling UPLC from TPLC/PIR/Plutus Tx, I'm not sure I like the idea of untangling UPLC from any kind of types. Built-in functions have signatures, those signatures have quantifiers, we should account for quantifiers somehow and force is a sensible way of doing that, semantics-wise. If we can get away with having minimal runtime/size overhead by pulling those forces out of the program, then I'll vote for not weirdifying the language. Particularly because such a change would be even trickier in the blockchain context where we have to maintain backwards compatibility or perform weird and potentially risky tricks.

I disagree with the reasoning in your argument. Semantics-wise, force makes no sense at all. The types in Plutus are meant to be erased away entirely, yet we have this vestigial force and delay, which is only there to preserve pseudo-laziness as experienced in Haskell in some edge cases with foralls. For comparison, GHC does not preserve foralls in the output (observable by doing (unsafeCoerce (id :: forall a. a -> a) :: Int -> Int) 5).

The real issue in my opinion is Plutus's reliance on impure behaviour. Even though Plutus is supposedly a functional language, you're supposed to cause a transaction failure by the script failing, an impure effect! Now, all of a sudden order of evaluation matters, when it should not have mattered in the first place. Of course, order of evaluation always matters in some sense, since one manner of evaluation might push the transaction past its allocated script budget, yet I believe that in practice, this is rare, as the programs we put in scripts aren't too complicated.

How would Plutus be made pure? Rather than failing invalid terms, make them stuck. Then, ifThenElse 0 1 2 would simply not reduce further and already be in WHNF. Script success can be done the same way: success is returning () (or True, perhaps), and any other WHNF is considered a failure. If a term is not in WHNF and the budget has been exceeded, that is of course also a failure.

In practice this would mean the pathological example of ifThenElse (nullList l) True (headList l) no longer behaves unexpectedly no matter the order of evaluation.
If evaluated strictly, if l is nil, then headList [] simply doesn't reduce, and the whole expression still returns True.

I believe this would allow entirely dropping all vestiges of call-by-name from the translation of Haskell into UPLC.

(Of course, you'd need a new language version, and existing Plutus scripts can't be trivially ported over, unless they're already in the idiomatic style which no one uses because of performance reasons.)

I considered this approach while thinking about replacing UPLC with an SKI calculus after revisiting https://okmij.org/ftp/tagless-final/ski.pdf for the 100th time.

---

As for the budget issue, this is still relevant, but even without this change it is quite honestly a huge pain the ass as you've likely already noticed.
I very much want to get rid of this, and as far as I can tell, there are these four general solutions:

• Make an interpreter in Plutus, such that a single transaction can push the script state forward without finishing.
• Allow creating transactions on Cardano that run an arbitrary script with an arbitrary context, while noting the resultant script state (i.e. hash of output term). Allow then chaining such transactions together, then finally consuming the output as a proof that your transaction would pass without running the script in its entirety in the final transaction. This would avoid the issues Duncan brought up at one time (don't remember where), that larger transaction budgets impede parallel processing of transactions. You could represent the outputs of the above-mentioned transactions as UTXOs.
• Cryptographically prove execution succeeds. Using a SNARK, that is, succinct non-interactive argument of knowledge, you would be able to prove that the execution succeeds with an exceedingly small probability of fraud (not unlike what Leios does). The issue is this is still nascent technology, and the practical solutions are still not developed. The current working ones are either 1) trustful or 2) too slow to verify proof/prove statement 3) size of proofs in bytes is too big. There are albeit papers exploring new theoretically practical solutions.
• Somehow prove that execution budget is not exceeded before you put the script on-chain. You can have types that express how much computation each term requires. This is not too complex in the absence of recursion, but still seems like a lot of novel work.

I still believe we should get rid of force and delay for new language versions entirely before we attempt to do any of the above.

[michaelpj]

This is all a bit of a digression, but...

I disagree with the reasoning in your argument. Semantics-wise, force makes no sense at all. The types in Plutus are meant to be erased away entirely, yet we have this vestigial force and delay, which is only there to preserve pseudo-laziness as experienced in Haskell in some edge cases with foralls.

This isn't quite right. Generally, polymorphism can be weird in strict languages if you erase the types entirely, because you can end up in a situation like this:

let x = /\ a . t
in ... x ...

===> erases to

let x = t
in ... x ...

and then we evaluate t as soon as we see it... but then we're effectively evaluating "under" the type abstraction and the semantics of our original language may not make sense there. This notoriously led to soundness issues in ML, and the traditional response is the "value restriction": terms underneath a type abstraction must be values and not things that can compute. This is a horrible artificial restriction also. We opted for a less traditional route in that we made type abstractions and applications have computational meaning. That removes the problem entirely, at the cost of having force and delay. That cost turns out to be more substantial in the end than we anticipated, but I just wanted to point out that the other points in the design space aren't good either.

Now, all of a sudden order of evaluation matters, when it should not have mattered in the first place.

Surprise! Order of evaluation does not matter today (apart from logging, which isn't observable on-chain). Since the only effect is error and the language is strict, changing the order of evaluation cannot affect whether or not you fail, it can only affect which failure you hit, and they're not distinguishable, so it doesn't matter.

If evaluated strictly, if l is nil, then headList [] simply doesn't reduce, and the whole expression still returns True.

I think this depends a lot on how we stuckness was handled. I see two approaches:

1. Propagate stuckness upwards. The rule for applications says "reduce your arguments to values, and then apply the function". If an argument is stuck, then you can't do that and the application is stuck. Then the ifThenElse is also stuck. But this is basically equivalent to having error!
2. Allow a stuck term to be passed around a value until we "need" it. I think this is arguably just making us weirdly non-strict in one place.

So I think this proposal is either equivalent to the status quo or a weird strict/non-strict hybrid.

[L-as]

I think 2. is the best solution. It is "weirdly" non-strict, but it solves the problem cleanly I think. You're right wrt. the rest FWIW. Rather than order of evaluation, perhaps saying evaluation matters even if you ignore its result? Which is essentially the same as saying it's impure.

The precise semantics would likely be something like this:

• Introduce new term stuck. This is a normal value and can be passed around as you expect. It is in some sense isomorphic to (), yet in TPLC we ascribe it every type, i.e. stuck :: a, not unlike undefined in Haskell.
• Applying something that isn't a function results in stuck.
• Applying a stuck to a lambda is not special-cased and is entirely valid.
• Applying a stuck to a built-in is stuck depending on whether the built-in uses it or not, i.e. when it checks which constructor (of e.g. Booleans) it is.
• In general, anything that generates an error now turns into stuck.

We get:

   ifThenElse (nullList Nil) True (headList Nil)
-> ifThenElse True True Stuck
-> True

   (\_ -> True) (headList Nil)
-> (\_ -> True) Stuck
-> True

(excuse me for not using the correct UPLC syntax, I can't remember it).

Perhaps the name "stuck" isn't quite right, because it's not possible to become unstuck (since there is nothing to wait for). The original term is entirely gone and replaced by something which is really just an error. The difference is entirely in how we handle the error.

In fact, you can describe the above as simply: Make error into a first-class value you can pass around, rather than bubbling it up immediately.

I will probably make a CIP as I believe this is IMO the cleanest solution.

I don't believe we have to remove delay and force from the language, albeit it may very well make the evaluator more efficient.
It would in any case allow you to omit those constructs entirely when erasing type abstractions and applications.

[effectfully]

@michaelpj

Allow a stuck term to be passed around a value until we "need" it. I think this is arguably just making us weirdly non-strict in one place.

I don't think is a strictness issue, it's an issue of breaking canonicity, where in our case "canonicity" means that evaluation of any closed term either produces a value in canonical form or diverges. With @L-as' proposal we'd have non-divergent non-canonical values. Which wouldn't be particularly unusual (those are normal when evaluating open terms or in a language with axioms/postulates), but it doesn't make for an appealing metatheory.

So I think this proposal is either equivalent to the status quo or a weird strict/non-strict hybrid.

Strict/non-strict hybrids are not necessarily weird and I remember proposing Plutus Core to be call-by-push-value (which supports both strict and non-strict) back in 2018.

@L-as how would (I'm horribly abusing the notation)

let factorial n = ifThenElse (n == 0) 1 (factorial (n - 1))
in factorial 2

evaluate with your proposal?

[L-as]

@effectfully It would diverge as expected.

[effectfully]

@L-as I don't understand the point then. You said

I believe this would allow entirely dropping all vestiges of call-by-name from the translation of Haskell into UPLC.

but if a basic if-then-else expression diverges unless we keep the existing machinery that prevents the two branches from being evaluated at the same time, then what problem are we trying to solve here with the introduction of stuck values?

[L-as]

but if a basic if-then-else expression diverges unless we keep the existing machinery that prevents the two branches from being evaluated at the same time

I don't believe we have any machinery to prevent this besides the compiler adding in lambdas (or delays) to the arguments, then forcing the result. This would not change.

[effectfully]

Sorry, I really don't get it. So given

In practice this would mean the pathological example of ifThenElse (nullList l) True (headList l) no longer behaves unexpectedly no matter the order of evaluation.

If evaluated strictly, if l is nil, then headList [] simply doesn't reduce, and the whole expression still returns True.

How is it unexpected that

ifThenElse (nullList l) True (headList l)

blows up but it's expected that

let factorial n = ifThenElse (n == 0) 1 (factorial (n - 1))
in factorial 2

loops?

[nielstron]

I am not sure how to proceed. I think the discussion kind of derailed on a related topic that is however not connected to this CIP. There also does not seem a strong position to keep the CIP (right now), so I am pondering if I should just leave it open to be considered at another point again or just close it? I think finalizing it does not make sense if there is no strong support to accept it.

[L-as]

#469

[michaelpj]

@nielstron Personally, I think it's useful to have Proposed CIPs that won't necessarily be accepted (@rphair I can't remember what we decided was the right way to do this?). Then in future if the discussion recurs we can refer to the previous proposal and see what we thought. So I would be keen for you to incorporate some of the discussion into the main text and then we can merge it.

[nielstron]

I have adjusted the proposal as per the comments.

[michaelpj]

To repeat my recommendation, I think it would be fine to merge this as Proposed.

[rphair]

@michaelpj I agree and would be inclined to merge this for reasons you mention in #459 (comment) since it seems the comments are now incorporated as of 0839537.

@nielstron the text you removed as "artifacts" in 27e4916 are in fact the canonical section titles as per CIP-0001: so if you would please put them back in as such (and fix the CIP header title, or if not then this PR title), I am ready to approve this.

[nielstron]

@rphair Thanks! Changes applied.

[rphair]

@Ryun1 @Crypto2099 this has been waiting for a 2nd editor review before merge since March 2023. Since all the discussion was settled as much as it ever could be (I think), and the last ruling from Plutus expertise was for this to stand as Proposed even though nobody will do it (#459 (comment)), I'm marking it Last Check to force it onto our meeting agenda & move it forward if no last objections: since it appears to be a proper proposal that just got lost between review requests.

[Ryun1]

@nielstron

Can you rename the folder for this proposal from CIP-???? to CIP-0091

[rphair]

@nielstron the only thing we're waiting for before approving & merging is you renaming the containing directory.

[nielstron]

Oh sorry, I missed that. I also adjusted the implementation plan to correctly note there is no plan to actually implement this CIP