Make the case arguments of matching functions in PlutusTx.Bulitins non-strict

[zliu41]

Dunno how this went unnoticed for so long, but obviously the case arguments shouldn't be strict.

[michaelpj]

No, I don't agree with this. It has always been this way, and they just have exactly the caveat that if you want to delay evaluation of one of the cases you need to match on () -> a or whatever and apply it afterwards. These are just Normal Functions, and so they are strict. And anyway, I thought tildes on argument patterns didn't do anything unless GHC inlined the function?

[bezirg]

We should perhaps write some comment that we should not use (~) in builtins and internals.
And that the user is responsible to non-strictify the arguments?

[Unisay]

Regardless of the final decision I think that we should provide unit tests that assert effects of strictness annotations either way, analogously to how lazyness/strictness in boolean operator False && error () influences evaluation results - this is testable (goldens aren't good for this purpose).

[effectfully]

Great catch. But this is one more argument in favor of Plutus Tx being weird.

[effectfully]

What??? This is a ridiculous optimization of memory usage.

[effectfully]

Why aren't those getting inlined?

[effectfully]

Good thing about pattern matching builtins is that they make this not only faster, but also quite shorter.

[effectfully]

Here we explicitly rely on GHC inlining this definition for us. Can we instead make sure to inline it ourselves (even though it's semantics-changing)? Is there a general rule? How many other such cases are we missing?

It sucks that we don't want GHC to touch our code much (because it doesn't understand the semantics), while at the time we want to rely on it in some cases.

[effectfully]

No, I don't agree with this. It has always been this way, and they just have exactly the caveat that if you want to delay evaluation of one of the cases you need to match on () -> a or whatever and apply it afterwards. These are just Normal Functions, and so they are strict. And anyway, I thought tildes on argument patterns didn't do anything unless GHC inlined the function?

I fully agree with you. But I agree with 53.2% -> 42.5% of max MEM even more.

[michaelpj]

I fully agree with you. But I agree with 53.2% -> 42.5% of max MEM even more.

I think this is just a path to making it totally impossible to reason about Plutus Tx code. I reluctantly agreed with the && case, but this is IMO just terrible. And it's unreliable since we're entirely at the mercy of GHC.

[zliu41]

@michaelpj Right, adding ~ to arguments doesn't matter. I wrote the doc about this but I keep forgetting 🤦‍♂️
Clearly this needs to be documented in the Haddock of matchList and matchData

[michaelpj]

Clearly this needs to be documented in the Haddock of matchList and matchData

And to the haddock of every single strict function we expose? Perhaps these are especially likely to trip people up, IDK 🤷

[zliu41]

Perhaps these are especially likely to trip people up, IDK 🤷

I think so - implementing !! for BuiltinList involves calling error for nilCase, which is what tripped me.

[effectfully]

@michaelpj

I think this is just a path to making it totally impossible to reason about Plutus Tx code. I reluctantly agreed with the && case, but this is IMO just terrible. And it's unreliable since we're entirely at the mercy of GHC.

I agree with all of that. But:

1. I already can't really reason about Plutus Tx code. Maybe it's an old habit though, the behavior of && was really confusing at times, but that is no longer the case
2. we're at the mercy of GHC here, but we're generally at its mercy, so why not benefit from the inevitable. GHC feels completely free to eta-expand functions for example and that changes the semantics for us. Should we insist on using pedantic-bottoms everywhere (perhaps yes)? Will it be enough (perhaps no)? Does GHC have a presimplifier or something of this sort? IIRC we cannot fully control GHC regardless, so if we can't, we don't have any option apart from trying to at least benefit from it some

If we can reliably reason about Plutus Tx code right now, then I'm not so sure we should do what we do here indeed.

[zliu41]

@effectfully What you said is the imo the biggest and most annoying problem with Plutus Tx. And I don't see how we can fix it, outside of introducing lazy evaluation for Plutus Core, so that GHC's transformations become valid from Plutus Tx point of view.

That said, I think we can view Plutus Tx as two different subsets of Haskell:

1. The subset that the plugin can compile
2. The (smaller) subset that not only the plugin can compile, but the resulting Plutus Core has the exact same semantic as the original Haskell. This requires making everything strict, among other things.

I think we should try and make the second subset as large as possible and encourage people to write Plutus Tx using the second subset. What I did in this PR (adding ~) makes the Haskell semantics deviate from the Plutus Core semantics which is not great.