PLT-4267: ADR: Plutus Tx's Evaluation Strategy, Compiler and Standard Library #5270
Conversation
zliu41
requested review from
bezirg,
michaelpj,
kwxm,
effectfully,
thealmarty and
a team
There was a problem hiding this comment.
I'm broadly on board. As a process note, I feel like this ADR has too many details (which probably belong in Notes in the code), rather than focussing on the decision at hand.
I'd also like to see some discussion of backwards compatibility. At least for switching to strict let-bindings by default. We'll probably need a plugin option to support people who want the old behaviour.
|
|
||
| - The conditional expression `if b then t else f` is always non-strict in `t` and `f`, like in most strict languages. | ||
| But what about `foo b t f = if b then t else f`? In a strict language, `foo` would be strict, and in a non-strict language, it would be non-strict. | ||
| But in Plutus Tx, due to how its compiler is currently implemented, whether `t` and `f` are evaluated strictly or not depends on whether GHC inlines `foo`. |
There was a problem hiding this comment.
This is also true in most strict languages, I think!
There was a problem hiding this comment.
@michaelpj you mean when forcing the inlining in a strict language?
There was a problem hiding this comment.
Is that really the case? In a strict language, when inlining foo b t f, I would expect it to produce let x=b, y=t, z=f in if x then y else z, which is still strict in t and f.
There was a problem hiding this comment.
Yes, you're right, sorry. The difference is that GHC can inline and then beta-reduce the application, and it's the beta-reduction that is different in GHC.
There was a problem hiding this comment.
I still think this is wrong as written. It's the beta-reduction that's different.
| Whenever the Plutus Tx compiler sees `let x = nonstrict rhs`, it first compiles `rhs` normally; then it creates a nonstrict binding in PIR: `let ~x = rhs_compiled`. | ||
|
|
||
| What if `x` gets inlined by GHC, i.e., GHC turns `let x = nonstrict rhs in ...x...` into `...(nonstrict rhs)...`? | ||
| That's not a problem, because if we see a `nonstrict rhs` that isn't the RHS of a binding, we create a new, non-strict binding from it, i.e., it becomes, in PIR, |
There was a problem hiding this comment.
It's a shame we can't just use this strategy unconditionally, i.e. it would be nice if we could turn
let x = nonstrict rhs in body
into
let ~fresh = rhs
in let !x = fresh
in body
but that doesn't actually work. Anyway, we can discuss the specific details elsewhere. In fact, I think probably this ADR shouldn't cover them: the decision is to handle this through explicit signalling that indicates a non-strict binding, and how we implement that isn't so relevant.
There was a problem hiding this comment.
We do need to agree that a reasonably good solution exists before we make the decision. I'll add to the ADR that the solution proposed is subject to change and is not part of the decision.
There was a problem hiding this comment.
In fact, I think this behaviour of nonstrict is actually pointless. There is no difference between ... t ... and let ~x = t in ... x .... In both cases we are going to evaluate t exactly when we hit the location where t is originally. So standalone nonstrict is pointless.
TBH I still don't love this approach. I don't like that we're putting something on the RHS of the binding to affect the LHS, and that it doesn't really have a standalone meaning or work anywhere else. I wish we could use an annotation or something, but source annotations can't be used on nested bindings :(
| It is not sufficient to create a non-strict binding for `go xs` (i.e., `let y = go xs in f x y`) because GHC will unconditionally inline `y`. | ||
|
|
||
| The problem can be solved by using `nonstrict`, replacing `f x (go xs)` with `f x (nonstrict (go xs))`. | ||
| Now `go xs` is evaluated non-strictly, and `foldr` can short-circuit. |
There was a problem hiding this comment.
I think we discussed this but this is not true! It's no good because your non-strict variable then gets used as a function argument to f, which means it gets evaluated. You have to also inline f, and to allow that you have to first inline foldr too.
Any time we have a higher-order function, the use of that function will be strict and we can't easily make it lazy.
There was a problem hiding this comment.
Oh yeah, that's right, it contradicts the gdrive
There was a problem hiding this comment.
Oh, right. Then we may need a second magical function, say nonstrictArg. Not ideal but it should work. I'll update the PR.
There was a problem hiding this comment.
@michaelpj Actually I think we can still use nonstrict. I updated the way the compiler deals with nonstrict and I think now it should work. Please take a look again at the paragraph starting with "What if x gets inlined by GHC" and see if you agree.
There was a problem hiding this comment.
No, it still doesn't work. None of these approaches will work in general. Function application is strict. There is no way around that, without inlining the function, which requires inlining foldr. The problem is not the beta optimization, the problem is function application. Seriously, work through the example. I'll pay attention if you can show it works :p
There was a problem hiding this comment.
Here's how it works: f x (go xs) normally becomes let !acc = go_xs_compiled in f x acc as a result of beta reduction.
But with f x (nonstrict (go xs)), it will annotate go_xs_compiled with NONSTRICT, and because of that annotation, beta-reduction, will create a nonstrict binding from it, i.e., let ~acc = go_xs_compiled in f x acc. Does that make sense?
There was a problem hiding this comment.
Okay, but now you have to evaluate the call to f (e.g. && in the case of all)... which will evaluate acc. So you have gained nothing.
There was a problem hiding this comment.
Hmm, right. Looking at anyCheap.plc.golden - it will make a difference if acc is nonstrict. But we do have foldr inlined here, which I guess is your point.
There was a problem hiding this comment.
Right, in that example we have inlined foldr and also f. Then, yes, we have a chance. But that's a pretty heavy requirement. And crucially, that's not a property of the argument to the function, but a property of the function itself (is it going to get inlined?). Making non-strict function application happen is already hard, and I think can only really be done by inlining the function, and we certainly can't do it by just doing something to the argument.
| def foo(a: Int, b: => Int) { ... } | ||
| ``` | ||
|
|
||
| `nonstrict` can be used to achieve a similar effect, except that `nonstrict` is used at the call sites as opposed to function definitions. |
There was a problem hiding this comment.
Again, I think this is wrong.
| The advantage of `Eval` is that it can be provided entirely in a library, without special compiler support. However, this is also what leads to its disadvantage: `Eval` is more heavyweight to use, since it changes the types of many functions (such as `foldr`), while `nonstrict` has the same type as the identity function, which is possible because it is a magical function that the compiler treats specially. | ||
|
|
||
| The takeaway is this: the standard libraries usually do the simple things, e.g., providing a monomorphic, non-short-circuiting version of `foldr` for lists, as well as functions like `all`, `any`, also monomorphically for lists. | ||
| The polymorphic versions of those functions, if exist, are usually provided by third-party libraries like cats. |
There was a problem hiding this comment.
I think Scala isn't a good example here: the standard library is sort of half-heartedly functional, one of the distinguishing features of cats is to try and be much more serious about Haskell-inspired functional programming.
There was a problem hiding this comment.
Yes, but AFAIK OCaml's foldr in its stdlib is also strict. It seems to make sense for a strict language to provide a strict foldr.
Also I'm not aware of a language that is perfectly analogous to Plutus Tx such that we can just copy what it does. E.g., for OCaml the choice is strict vs. lazy, but for Plutus Tx it is strict vs non-strict, which are totally different dynamics.
There was a problem hiding this comment.
for OCaml the choice is strict vs. lazy
I don't think that's right? I don't think OCaml has any lazy evaluation, so at best it's going to be non-strict?
There was a problem hiding this comment.
This paragraph is deleted in the new draft anyway, but OCaml has a lazy module that seems to provide machinery for lazy evaluation. I'm not at all familiar with OCaml so I may have misunderstood what it does.
|
|
||
| ### Monomorphizing Plutus Tx Standard Library | ||
|
|
||
| Strict languages do not lend themselves to code reuse, as there is a high cost to use abstractions such as higher-order functions and parametric polymorphism. |
There was a problem hiding this comment.
Why is parametric polymorphism expensive? Do you mean ad-hoc polymorphism (i.e. typeclasses)? If so that's not really about strict languages: GHC would have exactly the same overheads as we do (and often does!), but also goes to some lengths to eliminate dictionary passing.
There was a problem hiding this comment.
Yes, I meant ad-hoc polymorphism. I think it is more of a problem for strict languages. The example I had in mind was: it is difficult to implement a short-circuiting any :: Foldable t => (a -> Bool) -> t a -> Bool. So the cost of ad-hoc polymorphism in this case is the lack of short-circuiting.
I agree the dictionary thing is not unique to strict languages.
There was a problem hiding this comment.
Short-circuting is, in general, a pretty specific problem. Most uses of ad-hoc polymorphism don't particularly have anything to do with short-circuiting. It's pretty much only folding over lists with boolean operations where people expect this. So I think the framing is too harsh (and also I didn't get what it was saying, I assumed you must be talking about the budget cost of dictionary passing).
There was a problem hiding this comment.
See the updated draft, where this statement is removed.
| They can be implemented in terms of each other, so technically, only one of them needs to be in the `Foldable` class. | ||
| But certain types have more efficient direct implementations of `foldr`; the same for `foldMap`. | ||
| No matter which of them we move out of `Foldable`, it won't work optimally for certain types. | ||
| Keeping both in `Foldable` will cause `Foldable` to be a multiple method typeclass, which is expensive in and of itself, as explained above. |
There was a problem hiding this comment.
I'm going to be annoying and say: we should actually do budget benchmarks of the two versions and see. It's not obvious to me how much difference it makes!
There was a problem hiding this comment.
We already have proof that multiple method classes are expensive than single-method ones, unless I misunderstood what you meant by "the two versions"?
There was a problem hiding this comment.
I don't doubt they're more expensive, but how much?
There was a problem hiding this comment.
I fee like the discussion on the cost of multiple-method typeclasses is independent of the evaluation strategy discussion, so I removed it in the new draft.
|
|
||
| The idea is to make the Plutus Tx compiler perform GHC-like inlining for functions with the INLINE pragma. | ||
|
|
||
| "GHC-like inlining", or "inlining in the GHC way", for lack of a better term, refers to inlining in a way similar to how GHC does it, i.e., replacing a variable with its RHS, then performing beta substitution. |
There was a problem hiding this comment.
I'm confused by this. I don't think GHC's inliner actually does the substitution? I think the simplifier will do it, but I find it confusing to associate this with GHC's inlining somehow?
There was a problem hiding this comment.
I agree. I'm not sure how GHC draws the line exactly. To avoid confusion maybe we can just talk about the two ways of inlining explicitly:
(1) inlining AND performing the substitution
(2) only the inlining
There was a problem hiding this comment.
This is mainly a terminology issue. but look at the example below: by "GHC-like inlining", I mean getting the second result, which is what we'll get if we run GHC's inliner. Our own inliner will only give us the first result. Please suggest better terminology.
There was a problem hiding this comment.
I think what you're seeing there is due to the fact that GHC's inliner is just a part of the simplifier. So it's getting both inlined and simplified. I think it's confusing to call this "GHC-style inlining" since it isn't IMO. It's inlining-followed-by-semantically-incorrect-for-PIR-beta-reduction 😂
What I think this most looks like is macro-expansion. Indeed, that's what I've suggested in the past as a way to get short-circuiting behaviour: use macros (i.e. TH). You can very easily write a TH macro that expands inline the way you want it. And it's much less misleading, since it also clearly only works when you have the argument expressions to hand. Whereas your (&&) can be passed e.g. to a higher-order-function where it will not behave lazily with no indication of that.
As you can tell I'm pretty unconvinced by this proposal. I think it abuses the meaning of INLINE, and it's fragile and unreliable.
There was a problem hiding this comment.
See the new draft, where this part is rewritten.
| Normally, it is incorrect for the Plutus Tx compiler to inline `(&&)` in the GHC way, because in the `expr1 && expr2` example, before inlining, it evaluates `expr2` strictly, but after GHC-like inlining, `expr2` is evaluated non-strictly. | ||
| But because of the `INLINE` pragma, the Plutus Tx compiler should inline `(&&)` in the GHC way. | ||
| And this is desirable because we want `(&&)` to be non-strict. | ||
| Functions that should not be inlined in the GHC way should use the `INLINABLE` pragma. |
There was a problem hiding this comment.
Why shouldn't INLINE mean exactly what it means today? i.e. I'm not sure why this alternative meaning of inlining should get to claim the pragma, indeed I think that's surprising. We could use an alternative GHC annotation, perhaps?
There was a problem hiding this comment.
@michaelpj you mean this https://downloads.haskell.org/ghc/latest/docs/users_guide/extending_ghc.html?highlight=ann%20pragma#source-annotations ? That's a nice idea, and better than giving special meanings to INLINE/INLINEABLE pragmas
There was a problem hiding this comment.
Why shouldn't INLINE mean exactly what it means today?
INLINE should mean exactly what GHC means by INLINE. Which is different from what our inliner does. See the example above. We want the second result, not the first.
There was a problem hiding this comment.
hm....it does seem a bit confusing. So, if users want to define non-strict functions, they use the INLINE pragma. Otherwise, they use the INLINEABLE pragma, and it will be inlined with our PIR inliner?
There was a problem hiding this comment.
That's not what GHC means by INLINE. GHC means the same thing that we do. The fact that GHC's simplifier then inlines things is just a weird byproduct. INLINE should mean "inline this", nothing else.
There was a problem hiding this comment.
And yes, I think source annotations could be a good tool here.
There was a problem hiding this comment.
See the new draft where this part is rewritten.
doc/read-the-docs-site/adr/0005-plutus-tx-compiler-and-library.md
Outdated
Show resolved
Hide resolved
There was a problem hiding this comment.
I like this proposal a lot. We just have to make sure that all these great information and examples are properly catalogued in readthedocs.
One thing: since this is a fairly big semantic change, what happens to existing written PlutusTx scripts? Are we going to direct the plutustx users to use an older plutustx compiler version to retain the old behaviour or are we going to expose some extra plutus-tx-plugin flags to "control" this semantic change?
doc/read-the-docs-site/adr/0005-plutus-tx-compiler-and-library.md
Outdated
Show resolved
Hide resolved
| ## Background | ||
|
|
||
| Plutus Tx is a language for writing Plutus scripts. | ||
| It is a subset of Haskell and can be compiled to Untyped Plutus Core (hereafter referred to as PLC) by the Plutus Tx compiler, a GHC plugin. |
There was a problem hiding this comment.
We usually shorten it to UPLC?
There was a problem hiding this comment.
I find the U unnecessary here, especially since everything we say here about UPLC also applies to TPLC.
There was a problem hiding this comment.
It's not a big deal, I'm just wondering if we should be more consistent.
There was a problem hiding this comment.
We're super inconsistent 🤷
| And this is desirable because we want `(&&)` to be non-strict. | ||
| Functions that should not be inlined in the GHC way should use the `INLINABLE` pragma. | ||
|
|
||
| This has recently been partially done by @michaelpj [#5183](https://github.com/input-output-hk/plutus/pull/5183), which propagates `INLINE` pragmas but doesn't yet perform GHC-like inlining. |
There was a problem hiding this comment.
I think it would be nice to have a conclusion section that summarizes the take away and explains the next steps.
|
To be clear, at a high level I am pro the overall direction of:
I just have issues with the proposed mechanisms. |
| Plutus Tx is a language for writing Plutus scripts. | ||
| It is a subset of Haskell and can be compiled to Untyped Plutus Core (hereafter referred to as PLC) by the Plutus Tx compiler, a GHC plugin. | ||
|
|
||
| Haskell uses lazy evaluation (call by need) by default, while PLC is strict (call by value). |
There was a problem hiding this comment.
It's "call-by-need" and "call-by-value" in this context, I believe.
|
|
||
| Haskell uses lazy evaluation (call by need) by default, while PLC is strict (call by value). | ||
| This begs the question: what is the operational semantics of Plutus Tx? | ||
| This is an important question, the answer of which not only dictates how users of Plutus Tx should reason about and optimize their programs, but also has major implications on the design and implementation of the Plutus Tx compiler and libraries. |
There was a problem hiding this comment.
I'm very glad we're discussing this.
| - The conditional expression `if b then t else f` is always non-strict in `t` and `f`, like in most strict languages. | ||
| But what about `foo b t f = if b then t else f`? In a strict language, `foo` would be strict, and in a non-strict language, it would be non-strict. | ||
| But in Plutus Tx, due to how its compiler is currently implemented, whether `t` and `f` are evaluated strictly or not depends on whether GHC inlines `foo`. | ||
| Although we turn off GHC's inliner in the Plutus Tx compiler, GHC may still decide to unconditionally inline `foo` if it is used only once. |
There was a problem hiding this comment.
It stops doing so if one uses -fmax-simplifier-iterations=0.
There was a problem hiding this comment.
No. The plugin runs a simplifier pass itself, regardless of -fmax-simplifier-iterations.
There was a problem hiding this comment.
... and apparently I was wrong anyway.
| But what about `foo b t f = if b then t else f`? In a strict language, `foo` would be strict, and in a non-strict language, it would be non-strict. | ||
| But in Plutus Tx, due to how its compiler is currently implemented, whether `t` and `f` are evaluated strictly or not depends on whether GHC inlines `foo`. | ||
| Although we turn off GHC's inliner in the Plutus Tx compiler, GHC may still decide to unconditionally inline `foo` if it is used only once. | ||
| In general, it is not easy to predict whether GHC will inline something or not. |
There was a problem hiding this comment.
It's easy if you turn off all GHC optimization. RV didn't want any inlining whatsoever and turning off all GHC optimization with -fmax-simplifier-iterations=0 worked for them.
| Plutus Tx should be a strict-by-default language. | ||
| Non-strict-by-default languages are rarely used in practice since non-strict evaluation leads to repeated evaluations. |
There was a problem hiding this comment.
I think there's a lot of terminology confusion here.
- strict vs non-strict isn't about evaluation per se, that distinction lies within the realms of denotational semantics. E.g.
seqis strict in both of its arguments, which doesn't tell us much about how things evaluate - call-by-value is an evaluation strategy that a strict language can adopt. Similarly, call-by-name or call-by-need are evaluation strategies that a non-strict language can adopt. At this level we're talking about the operational semantics of a language. For
seqwe'd say that it's supposed to evaluate its second argument after evaluating the first one. However if GHC devs were to makeseqevaluate both of its arguments in parallel, that would still comply with the denotational specification of the function - eager vs lazy is fairly vague terms for describing the specific implementation of the evaluation strategy of a language
As such, non-strictness doesn't lead to any repeated evaluation as it isn't about evaluation at all. Laziness can lead to repeated evaluation if the call-by-name evaluation strategy is chosen, but that's horrible enough for it to be very uncommon (Agda used to be call-by-name for an example, not sure how far they've gone in making it call-by-need instead). In practice lazy languages implement call-by-need (Haskell, R) and that doesn't lead to repeated evaluation.
There was a problem hiding this comment.
Thanks, this is good to know! So I considered primarily mentioning evaluation strategies (call-by-X) and avoid mentioning evaluation orders (strict/nonstrict), since our chief concern is performance, and it is the operational semantics that matters.
However, given that there are only two possible evaluation strategies for Plutus Tx: call-by-value (if strict) and call-by-name (if non-strict), strict/non-strict implies call-by-value/call-by-name. So I decided to still primarily mention strict/non-strict in the article as it reads better for me that way (especially since some parts of the discussion only care about denotation), but with some clarification upfront. Let me know what you think.
|
|
||
| Plutus Tx should be a strict-by-default language. | ||
| Non-strict-by-default languages are rarely used in practice since non-strict evaluation leads to repeated evaluations. | ||
| Unless we implement lazy evaluation for PLC in the future, strictness should be the default for Plutus Tx. |
|
|
||
| ### Making Let-bindings Strict By Default | ||
|
|
||
| In a strict-by-default language, it would make sense that let-bindings be strict by default, since that's what almost all strict languages do; plus, non-strict bindings should be used cautiously since they can easily lead to unbounded amount of repeated evaluation. |
There was a problem hiding this comment.
Unless non-strict bindings are backed by a sensible evaluation strategy. Which isn't our case, yes.
| Haskell supports lazy patterns with the `~` operator, and it can be used on let-bindings, e.g., `let ~x = rhs`. So one possibility is to make non-strict let-bindings this way. | ||
| However, lazy pattern has no effect on simple pattern bindings (i.e., the pattern is a single variable), and it makes no difference in GHC Core, which means the Plutus Tx compiler can't actually see the `~`. | ||
| It is technically possible to make `~` work but it would require adding a GHC parser plugin to capture `~` in GHC Core, among other things, adding a great deal of complexity. |
There was a problem hiding this comment.
Can't we just enable the Strict pragma by default and then use let ~x = rhs? Quoting the docs:
Informally the
Strictlanguage extension switches functions, data types, and bindings to be strict by default, allowing optional laziness by adding~in front of a variable. This essentially reverses the present situation where laziness is default and strictness can be optionally had by adding!in front of a variable.
There was a problem hiding this comment.
Good question, I didn't consider StrictData. But how can we enable StrictData by default? It can probably be done in a DynFlags plugin, but that means using another plugin.
There was a problem hiding this comment.
Not StrictData, Strict. Strict is super weird and almost nobody uses it. I guess we could try it, but it would be invasive, and require changing the compilation flags of modules the plugin doesn't run on, perhaps 🤔 We could just say "we recommend using Strict" quite clearly and use it in our examples and libraries? Worth an experiment at least.
| In a strict-by-default language, it would make sense that let-bindings be strict by default, since that's what almost all strict languages do; plus, non-strict bindings should be used cautiously since they can easily lead to unbounded amount of repeated evaluation. | ||
| But if make let-bindings strict by default, then the question is, how does one make a non-strict let-binding? | ||
|
|
||
| Haskell supports lazy patterns with the `~` operator, and it can be used on let-bindings, e.g., `let ~x = rhs`. So one possibility is to make non-strict let-bindings this way. |
There was a problem hiding this comment.
I'd either use "irrefutable patterns" or "lazy matching". "lazy patterns" sounds weird to me, but maybe it's just me.
@bezirg has a good point. We should probably discuss the implications for existing scripts in the ADR? |
There was a problem hiding this comment.
and if possible some kinds of non-strict functions
@michaelpj looks like this non-strict functions thing isn't going to work, unless, like you said, we add INLINE to a lot of functions but that can lead to explosion of script sizes. The only other option I can see is to provide some kind of non-strict application support in the evaluator, but that comes with all kinds of other issues.
And this means there's no good way to implement any :: Foldable t => (a -> Bool) -> t a -> Bool such that it reliably short circuits.
As such I'll delete the sections about non-strict functions. With regard to the stdlib, I think we can provide a non-short-circuiting foldr, and then implement monomorphic any etc. for lists and other concrete types, without using foldr - like some other languages do. Does that make sense?
| Haskell supports lazy patterns with the `~` operator, and it can be used on let-bindings, e.g., `let ~x = rhs`. So one possibility is to make non-strict let-bindings this way. | ||
| However, lazy pattern has no effect on simple pattern bindings (i.e., the pattern is a single variable), and it makes no difference in GHC Core, which means the Plutus Tx compiler can't actually see the `~`. | ||
| It is technically possible to make `~` work but it would require adding a GHC parser plugin to capture `~` in GHC Core, among other things, adding a great deal of complexity. |
There was a problem hiding this comment.
Good question, I didn't consider StrictData. But how can we enable StrictData by default? It can probably be done in a DynFlags plugin, but that means using another plugin.
Yeah, I think that's the only option, really. |
There was a problem hiding this comment.
@michaelpj @effectfully I did a major rewrite based on the comments. Please take another look.
| - The conditional expression `if b then t else f` is always non-strict in `t` and `f`, like in most strict languages. | ||
| But what about `foo b t f = if b then t else f`? In a strict language, `foo` would be strict, and in a non-strict language, it would be non-strict. | ||
| But in Plutus Tx, due to how its compiler is currently implemented, whether `t` and `f` are evaluated strictly or not depends on whether GHC inlines `foo`. | ||
| Although we turn off GHC's inliner in the Plutus Tx compiler, GHC may still decide to unconditionally inline `foo` if it is used only once. |
There was a problem hiding this comment.
No. The plugin runs a simplifier pass itself, regardless of -fmax-simplifier-iterations.
| Plutus Tx should be a strict-by-default language. | ||
| Non-strict-by-default languages are rarely used in practice since non-strict evaluation leads to repeated evaluations. |
There was a problem hiding this comment.
Thanks, this is good to know! So I considered primarily mentioning evaluation strategies (call-by-X) and avoid mentioning evaluation orders (strict/nonstrict), since our chief concern is performance, and it is the operational semantics that matters.
However, given that there are only two possible evaluation strategies for Plutus Tx: call-by-value (if strict) and call-by-name (if non-strict), strict/non-strict implies call-by-value/call-by-name. So I decided to still primarily mention strict/non-strict in the article as it reads better for me that way (especially since some parts of the discussion only care about denotation), but with some clarification upfront. Let me know what you think.
| Haskell supports lazy patterns with the `~` operator, and it can be used on let-bindings, e.g., `let ~x = rhs`. So one possibility is to make non-strict let-bindings this way. | ||
| However, lazy pattern has no effect on simple pattern bindings (i.e., the pattern is a single variable), and it makes no difference in GHC Core, which means the Plutus Tx compiler can't actually see the `~`. | ||
| It is technically possible to make `~` work but it would require adding a GHC parser plugin to capture `~` in GHC Core, among other things, adding a great deal of complexity. |
| It is not sufficient to create a non-strict binding for `go xs` (i.e., `let y = go xs in f x y`) because GHC will unconditionally inline `y`. | ||
|
|
||
| The problem can be solved by using `nonstrict`, replacing `f x (go xs)` with `f x (nonstrict (go xs))`. | ||
| Now `go xs` is evaluated non-strictly, and `foldr` can short-circuit. |
| The advantage of `Eval` is that it can be provided entirely in a library, without special compiler support. However, this is also what leads to its disadvantage: `Eval` is more heavyweight to use, since it changes the types of many functions (such as `foldr`), while `nonstrict` has the same type as the identity function, which is possible because it is a magical function that the compiler treats specially. | ||
|
|
||
| The takeaway is this: the standard libraries usually do the simple things, e.g., providing a monomorphic, non-short-circuiting version of `foldr` for lists, as well as functions like `all`, `any`, also monomorphically for lists. | ||
| The polymorphic versions of those functions, if exist, are usually provided by third-party libraries like cats. |
There was a problem hiding this comment.
This paragraph is deleted in the new draft anyway, but OCaml has a lazy module that seems to provide machinery for lazy evaluation. I'm not at all familiar with OCaml so I may have misunderstood what it does.
|
|
||
| The idea is to make the Plutus Tx compiler perform GHC-like inlining for functions with the INLINE pragma. | ||
|
|
||
| "GHC-like inlining", or "inlining in the GHC way", for lack of a better term, refers to inlining in a way similar to how GHC does it, i.e., replacing a variable with its RHS, then performing beta substitution. |
There was a problem hiding this comment.
See the new draft, where this part is rewritten.
| Normally, it is incorrect for the Plutus Tx compiler to inline `(&&)` in the GHC way, because in the `expr1 && expr2` example, before inlining, it evaluates `expr2` strictly, but after GHC-like inlining, `expr2` is evaluated non-strictly. | ||
| But because of the `INLINE` pragma, the Plutus Tx compiler should inline `(&&)` in the GHC way. | ||
| And this is desirable because we want `(&&)` to be non-strict. | ||
| Functions that should not be inlined in the GHC way should use the `INLINABLE` pragma. |
There was a problem hiding this comment.
See the new draft where this part is rewritten.
|
|
||
| ### Monomorphizing Plutus Tx Standard Library | ||
|
|
||
| Strict languages do not lend themselves to code reuse, as there is a high cost to use abstractions such as higher-order functions and parametric polymorphism. |
There was a problem hiding this comment.
See the updated draft, where this statement is removed.
| They can be implemented in terms of each other, so technically, only one of them needs to be in the `Foldable` class. | ||
| But certain types have more efficient direct implementations of `foldr`; the same for `foldMap`. | ||
| No matter which of them we move out of `Foldable`, it won't work optimally for certain types. | ||
| Keeping both in `Foldable` will cause `Foldable` to be a multiple method typeclass, which is expensive in and of itself, as explained above. |
There was a problem hiding this comment.
I fee like the discussion on the cost of multiple-method typeclasses is independent of the evaluation strategy discussion, so I removed it in the new draft.
| - The conditional expression `if b then t else f` is always non-strict in `t` and `f`, like in most strict languages. | ||
| But what about `foo b t f = if b then t else f`? In a strict language, `foo` would be strict, and in a non-strict language, it would be non-strict. | ||
| But in Plutus Tx, due to how its compiler is currently implemented, whether `t` and `f` are evaluated strictly or not depends on whether GHC inlines `foo`. | ||
| Although we turn off GHC's inliner in the Plutus Tx compiler, GHC may still decide to unconditionally inline `foo` if it is used only once. |
There was a problem hiding this comment.
... and apparently I was wrong anyway.
| But what about `foo b t f = if b then t else f`? In a strict language, `foo` would be strict, and in a non-strict language, it would be non-strict. | ||
| But in Plutus Tx, due to how its compiler is currently implemented, whether `t` and `f` are evaluated strictly or not depends on whether GHC inlines `foo`. | ||
| Although we turn off GHC's inliner in the Plutus Tx compiler, GHC may still decide to unconditionally inline `foo` if it is used only once. | ||
| In general, it is not easy to predict whether GHC will inline something or not. |
| Plutus Tx should be a strict-by-default language, mainly because it cannot currently use call-by-need (lazy) evaluation. | ||
| If it was non-strict by default, call-by-name evaluation would be the default evaluation strategy. | ||
| Call-by-name is rarely used in practice since it leads to repeated evaluations. | ||
| Unless we implement call-by-need evaluation for PLC in the future, strictness should be the default for Plutus Tx. |
|
|
||
| Haskell supports irrefutable patterns with the `~` operator, and it can be used on let-bindings, e.g., `let ~x = rhs`. So one possibility is to make non-strict let-bindings this way. | ||
| However, irrefutable patterns have no effect on simple pattern bindings (i.e., the pattern is a single variable), and it makes no difference in GHC Core, which means the Plutus Tx compiler can't actually see the `~`. | ||
| It is technically possible to make `~` work but it would require adding a GHC parser plugin to capture `~` in GHC Core, among other things, adding a great deal of complexity. |
There was a problem hiding this comment.
This doesn't consider the option of enabling Strict?
| One argument against this is that a module may contain both on-chain and off-chain code, some modules contain off-chain code only, and the same piece of code may be both on-chain and off-chain. | ||
| For off-chain code one typically doesn't want to enable `Strict`. | ||
|
|
||
| Another disadvantage of using `Strict` is that it may cause GHC to do additional optimizations in ways that can break the Plutus Tx compiler. |
There was a problem hiding this comment.
Kinda embarrassing, even though not our fault in any way.
| Then, to create a non-strict let-binding, we write | ||
|
|
||
| ```haskell | ||
| let x = nonstrict rhs in body |
There was a problem hiding this comment.
We could reuse GHC.Magic.lazy if we wanted to.
| force a = a () | ||
|
|
||
| class Foldable_Delay t where | ||
| foldr_delay :: (a -> Delay b -> Delay b) -> Delay b -> t a -> Delay b |
There was a problem hiding this comment.
Looks like it can work with just
foldr_delay :: (a -> Delay b -> b) -> Delay b -> t a -> b?
doc/read-the-docs-site/adr/0005-plutus-tx-compiler-and-library.md
Outdated
Show resolved
Hide resolved
Co-authored-by: effectfully <[email protected]>
| ## Background | ||
|
|
||
| Plutus Tx is a language for writing Plutus scripts. | ||
| It is a subset of Haskell and can be compiled to Untyped Plutus Core (hereafter referred to as PLC) by the Plutus Tx compiler, a GHC plugin. |
There was a problem hiding this comment.
We're super inconsistent 🤷
|
|
||
| Unfortunately, this question is currently difficult to answer. | ||
| Note that there are only two possible evaluation strategies for Plutus Tx: (strict evaluation, call-by-value) and (non-strict evaluation, call-by-name). | ||
| In parcitular, Plutus Tx cannot use call-by-need because PLC's evaluator (the CEK machine) has no support for thunks and memoization. |
There was a problem hiding this comment.
| In parcitular, Plutus Tx cannot use call-by-need because PLC's evaluator (the CEK machine) has no support for thunks and memoization. | |
| In particular, Plutus Tx cannot use call-by-need because PLC's evaluator (the CEK machine) has no support for thunks and memoization. |
| This is an important question, the answer of which not only dictates how users of Plutus Tx should reason about and optimize their programs, but also has major implications on the design and implementation of the Plutus Tx compiler and libraries. | ||
|
|
||
| Unfortunately, this question is currently difficult to answer. | ||
| Note that there are only two possible evaluation strategies for Plutus Tx: (strict evaluation, call-by-value) and (non-strict evaluation, call-by-name). |
There was a problem hiding this comment.
what about "totally inconsistent" like today 😂
|
|
||
| - The conditional expression `if b then t else f` is always non-strict in `t` and `f`, like in most strict languages. | ||
| But what about `foo b t f = if b then t else f`? In a strict language, `foo` would be strict, and in a non-strict language, it would be non-strict. | ||
| But in Plutus Tx, due to how its compiler is currently implemented, whether `t` and `f` are evaluated strictly or not depends on whether GHC inlines `foo`. |
There was a problem hiding this comment.
I still think this is wrong as written. It's the beta-reduction that's different.
| We have a few options: | ||
|
|
||
| 1. Do nothing, and encourage people to use the `Strict` GHC extension, which makes let-bindings strict by default. | ||
| This is not technically "strict by default", since the `Strict` extension is off by default, but it is still ergonomically better than using bang patterns on every binding. |
There was a problem hiding this comment.
I see what you're saying, it's a bit subtle though. It makes the surface language that the users write strict by default... but they have to do something to achieve that 🤷
| As a result, in addition to `Strict`, one may need to also use one or more of the following GHC flags: `-fno-strictness`, `-fno-specialise`, `-fno-spec-constr`, `-fno-unbox-strict-fields`, `-fno-unbox-small-strict-fields`. | ||
| Not only is it inconvenient, but failing to do so may lead to obscure compilation errors. | ||
| 2. Enable `Strict` automatically. | ||
| This can be done in a GHC driver plugin. |
There was a problem hiding this comment.
This is missing the other big downside I pointed out in the meeting. In order for a plugin to be active on a module, you have to turn it on. So you would have to turn on, manually, on all the modules you use transitively from your on-chain code. Or you put it in global ghc-options. But if you're doing that... you could just turn on Strict!
| - This is a critical one: it is susceptible to GHC inlining bindings unconditionally. | ||
| If GHC decides to turn `let x = rhs in ...x...` into `...rhs...`, then `x` effectively becomes non-strict, and there's nothing the Plutus Tx compiler can do to recover `x`. | ||
|
|
||
| If we can modify the Plutus Tx compiler such that we can turn off GHC's pre-inliner (which will be discussed later), then option 3 becomes the most preferrable. |
There was a problem hiding this comment.
I think this points to an under-appreciated benefit of option 1: if we can persuade GHC that the source language is strict, then we should have to worry a lot less in general about GHC mis-optimizing things, because GHC should have a compatible view of the world to us.
| It would be useful to allow user-defined non-strict functions, so that we can define functions like `&&` and `||` that short-circuit properly. | ||
| Some languages like Scala have special syntaxes for defining non-strict functions; we can't change Haskell's syntax, so we need to find a different solution. | ||
|
|
||
| The idea is to make the Plutus Tx compiler perform inlining and beta reduction for functions with INLINE pragmas, i.e., the same as how GHC treats INLINE pragmas. |
There was a problem hiding this comment.
I'm sorry, I still hate it 😬 I really don't want to use INLINE for this. I'd be more happy to use a custom source annotation as previously discussed, although I still very much don't love it.
|
|
||
| ### Turning off GHC's pre-inliner | ||
|
|
||
| As said before, one reason why the semantics of Plutus Tx is difficult to predict is because we run GHC's pre-inliner, which may perform unconditional inlining. |
There was a problem hiding this comment.
Of course, if we get GHC to agree with us that the language is strict, then we shouldn't have to worry about this so much, no?
zeme-wana
force-pushed
the
master
branch
2 times, most recently
from
a161078
to
db5cabb
Compare
There was a problem hiding this comment.
I failed to review this at the time (April 2023!) and now I have no idea what the status is: it seems that there's a version of this document merged already and I don't know how these changes relate to that.
Anyway, this has been on my list of outstanding GitHub review requests for a long time and I'm making this comment to get rid of it.
No description provided.