Add let binding to UPLC?

[L-as]

Describe the feature you'd like

Currently, in Plutarch (and I assume same for PlutusTx), we're emulating let bindings let x = y; z as (\x -> z) y, but this has the cost of introducing then eliminating a lambda.
If we had a Let constructor or similar, it's possible that it would be faster to interpret common scripts, if they were made to use native let-bindings.

Describe alternatives you've considered

No response

[michaelpj]

The whole point of PLC is to be very low level and not include such things. It sounds like you're gradually re-inventing PIR, which exists exactly to add types, (recursive) let-bindings, and datatypes :)

[L-as]

The point is to increase performance of scripts.

[michaelpj]

Why do you think it would be faster? In both cases most of the work is evaluating the RHS and putting it into the environment.

[L-as]

Smaller AST.

[michaelpj]

Here's my more detailed analysis.

First, what happens when we evaluate the two versions?

[ (\x . t) a ]

• Compute [ ... ]
• Compute \x . t
• Return \x.t
• Compute a
• Return a
• Apply

let x = a in t

• Compute let ...
• Compute a
• Return a
• Apply

So indeed let would let us avoid computing and returning the lambda, because it's as if we statically know that we're applying a lambda and not an arbitrary term that needs evaluating.

So what does this save us? One compute-return step per let-binding, which corresponds to:

1. A pattern match
2. A couple of function calls
3. One step of costing
4. Allocating a lambda abstraction value

Of these we have evidence that 4 makes some difference from #5042, but we can also avoid that by doing something like the optimization in that PR. The others are very cheap except for 3, which might matter.

The other factor is that it depends how hot (i.e. frequently evaluated) let-bindings are. My belief is that they are currently not that hot, see below for reasoning.

---

We can use the sums-of-products work as a convenient testbed for this. Sums-of-products introduces a bunch of immediately-applied lambdas whenever we evaluate a pattern match. This could instead be let-terms. Moreover, I implemented two versions of sums-of-products, one where case expressions bind variables, and one where they just apply lambdas. The former corresponds to having let-terms.

The version which bound variables had about a 10% speedup over the one that didn't, but we could reclaim 5% of it with #5042, i.e. cause 4 above seems to account for half of the wastage, and is independently fixable. But that PR makes only a 2% difference on master, which also tells us that sums-of-products introduces far more let-term opportunities than exist on master.

---

Regarding multi-lets versus multi-lambdas: I believe this would dilute the advantage of multi-lets even further. The advantage of let is just that it lets us avoid evaluating the lambda; but with multi lambdas we still only do one lambda evaluation, but this time for multiple arguments. So the overhead is proportionally less. In all other respects I'd expect them to have the same behaviour.

---

Summing up:

• I believe this is not a big deal on master
• I think it will become a bigger deal with sums-of-products
• My informed guess is that the speedup from adding lets would be on the order of 5% (assuming we do something like Don't allocate VLamAbs and VDelay if we don't need to #5042, otherwise it would be more like 10%)
• Multi-lambdas reduce the advantage further
• Overall I don't think this is worth the complication of adding a new language construct

[effectfully]

I'm going to claim that:

1. this appears to be a low priority issue
2. it doesn't seem like we definitely have a "won't do" here

Hence I'm adding the low priority label and keeping the issue open.

[colll78]

From my perspective, this is a very big deal. Using a let while folding on inputs / outputs is very common. 10% is very significant (and tests that I have done approximate the efficiency benefits at ~13-16%). The complexity of this language construct seems relatively low in comparison.

[effectfully]

@colll78 I do also like the idea of adding let to the language. Not sure if it's worth adding multi-lets, given that it's probably even more indirections than just iterating a single let. But we're generally very cautious when it comes to extending the AST of the language, so it would be great to have more data on the usefulness of let (we did perform a bunch of investigation regarding multi-lambdas).

(and tests that I have done approximate the efficiency benefits at ~13-16%)

Please consider sharing those, that can potentially help us quite a bit.

[michaelpj]

Yes, I would like to see the evidence. As I argued above, I'm not as convinced of the benefits.

[effectfully]

I've spent some time thinking about it and I believe we should definitely try adding let to UPLC and optimize applied lambdas to iterated lets (I don't think multi-lets would be faster than iterated lets, but maybe I'm wrong). Evaluating let should take fewer CEK machine cycles than evaluating an applied lambda and we sure evaluate a lot of applied lambdas, particularly given that all recursion is applied lambdas.

[effectfully]

If we don't add a let (which I think we should), then we should at least consider rendering applied lambdas as lets.

Currently we pretty-print applied lambdas as:

(\x1 ->
    (\x2 ->
        (\x3 -> body)
          e3
      e2
  e1

which is ok in this small example, but in a bigger one it’s a lot of unnecessary indentation, the “RHS” of the variable can be very far from its LHS and the whole thing is generally quite unreadable, especially when some of the application are iterated (check it out yourself by reading the program in this comment). This makes it harder than necessary to read the output of the readable pretty-printer, which has negative consequences:

• we are less keen to actually dive into golden tests and make sure they’re correct
• any kind of interaction involving Plutus Core code takes more time than it could. Be it an internal discussion or an external report or literally anything – any Plutus Core snippet slows down the conversation just because of the effort it takes to understand the snippet

This ticket is for changing the pretty-printer to render the above term as

let
  x1 = e1
  x2 = e2
  x3 = e3
in 
  body

or something similar.

We’ve done a lot to make Plutus Core readable and it did help. Rendering applied lambdas as lets will make reading Plutus Core scripts even more manageable, making us overall a bit more productive.

[colll78]

can be very far from its LHS and the whole thing is generally quite unreadable, especially when some of the application are iterated (check it out yourself by reading the program in this comment). This makes it harder than necessary to read the output of the readable pretty-printer, which has negative consequences:

• we are less keen to actually dive into golden tests and make sure they’re correct
• any kind of interaction involving Plutus Core code takes more time than it could. Be it an internal discussion or an external report or literally anything – any Plutus Core snippet slows down the conversation just because of the effort it takes to understand the snippet

A great reference you can use for really nice UPLC pretty printing is:
https://github.com/Plutonomicon/plutarch-plutus/blob/f78b70eca8841a4a009cb6791a59c999cbc68745/Plutarch/Pretty.hs#L42

It does exactly what you are describing (rendering applied lambdas as lets) ie:

• The AST structure produced by plet (Single Apply + LamAbs pair) is prettified into Haskell-like let bindings.
• Lazy if/then/else (pif in particular, not pif') is detected and prettified into Haskell-like syntax:
  if cond then expr1 else expr2.

let frSndPair = !!sndPair
    unDataSum = (\xF -> frSndPair (unConstrData xF))
    frTailList = !tailList
    frHeadList = !headList
    frIfThenElse = !ifThenElse
in (\oP4ECBT qsrxlF0Y7 ->
      let cjlB6yrGk = unDataSum qsrxlF0Y7
          cRFO = unConstrData (frHeadList (frTailList cjlB6yrGk))
          cs9iR = !!fstPair cRFO
          w4 = frSndPair cRFO
      in

It also does a ton of other stuff that makes the UPLC much more readable including:

Lambdas are prettified similar to haskell lambdas, i.e \x -> ....
Lambdas with multiple arguments are detected and simplified: \x y z -> ....
Application is, simply, a space - just like haskell. f x.
Multi arg applications to the same function are detected and simplified: f x y.

[effectfully]

@colll78 thank you for the reference. I'm particularly glad that others do this, because we've had some debates internally whether it's weird or not to render applied lambdas as lets.

It also does a ton of other stuff that makes the UPLC much more readable including:

Lambdas are prettified similar to haskell lambdas, i.e \x -> ....
Lambdas with multiple arguments are detected and simplified: \x y z -> ....
Application is, simply, a space - just like haskell. f x.
Multi arg applications to the same function are detected and simplified: f x y.

We have all of that in the form of an alternative Agda-like syntax called "readable". Here's an example in the typed lang:

/\a b c ->
  \(f : a -> b -> c) (p : pair a b) -> f (fstPair {a} {b} p) (sndPair {a} {b} p)

[effectfully]

We're moving tickets from Jira, so here's some context that we had there (written by me, so biased in favor of adding lets) but not here:

A human thinks of a let differently than they think of an applied lambda leading to missed opportunities (here’s one example, here’s another one). For three, evaluating a let is more efficient than evaluating an applied lambda.

As for having iterated lets, it’s probably not worth it, since it’ll only introduce more indirections in the AST and the evaluator.

Adding a non-iterated let seems to be low-cost and clearly helpful, so I don’t see why we shouldn’t do it.

[michele-nuzzi]

I'm sure it is already mentioned

but reporting that case and contr now are almost native lets

#6584 (comment)