plutus icon indicating copy to clipboard operation
plutus copied to clipboard

Short circuit ops for booleans (over QQ)

Open anton-k opened this issue 3 years ago • 3 comments

Fixes #4114

The problem is that plutus booleans don't use short circuit on evaluation. There is ugly fix to rewrite all expressions with if-then-else. But code becomes rather clumsy. We can fix that with meta TH.

Proposed fix defines two qq-functions and_if and or_if:

[and_if| expr1, expr2, expr3]

for arbitrary number of arguments is expanded to

if expr1
  then if expr2
    then if expr3
      then True
      else False
    else False
  else False 

and

[or_if| expr1, expr2, expr3]

is expanded to

if expr1
  then True
  else if expr2
    then True
    else if expr3
      then True
      else False

anton-k avatar Nov 05 '21 15:11 anton-k

I think I'd rather have the simpler typed-TH version, no need for quasiquotation parser failure or anything like that.

andLazy :: [ TExpQ Bool ] -> TExpQ Bool
andLazy [] = [|| True ||]
andLazy (e:es) = [|| if $$e then $$(andTH es) else False ||]

orLazy :: [ TExpQ Bool ] -> TExpQ Bool
orLazy [] = [|| False ||]
orLazy (e:es) = [|| if $$e then True else $$(orTH es) ||]

example :: Bool
example = $$(andTH [ [|| True ||] [|| False ||])

Location looks fine. Would be nice to have a test witnessing the lazy behaviour.

michaelpj avatar Nov 05 '21 15:11 michaelpj

@michaelpj Ok, I've added tests, for simple cases and to prove the lazy evaluation. To me it's more to type and clutter every case with [| ... |] [| ... |] for simple TH solution, than to write once [op|.. |] for QQ one.

anton-k avatar Nov 05 '21 16:11 anton-k

There is a bit of problem with multiline versions. If there is type-checker error in one of the parts of the expressions like in:

[and_if|
  True,
  False,
  () == False
|]

It will report line of the error as beginning of the and_if.

anton-k avatar Nov 05 '21 16:11 anton-k

@michaelpj can we simply define

(&&) :: Bool -> Bool -> Bool
(&&) = \x y -> if x then y else False
{-# INLINE (&&) #-}

This is pretty much guaranteed to get inlined and we'll get the right short-circuiting semantics as long as GHC doesn't attempt to optimize the resulting if expression while reducing the lambdas statically. Or am I missing something?

Although maybe

(&&) :: Bool -> Bool -> Bool
x && y = if x then y else False
{-# INLINE (&&) #-}

would be a bit more reliable?

effectfully avatar Feb 15 '23 04:02 effectfully

We could do that. My main concern was that then we have surprising behaviour in a different way: we have a function call where the arguments are not evaluated strictly! That's also surprising. But maybe it's less surprising, I don't really know.

(Both your variant should be the same in PIR)

michaelpj avatar Feb 15 '23 09:02 michaelpj

We could do that. My main concern was that then we have surprising behaviour in a different way: we have a function call where the arguments are not evaluated strictly! That's also surprising. But maybe it's less surprising, I don't really know.

(Both your variant should be the same in PIR)

That sounds kind of bad, like following a lesser of two evils approach

bezirg avatar Feb 16 '23 11:02 bezirg