Speed up heavy use of mapTotalResult

[MaximilianAlgehed]

@nick8325 we are very confused about what's going on here. mapTotalResult results in repeated calls to property on something of type Property. This in turn results in repeated layers of protectProp which causes properties that do a lot of tabulate or other similar things to blow up.

Now, our intuition is that it should be fine to only do the protectProp once, when we run the property. Is this correct? What was the reason for the convoluted instance? No tests fail if you just do property = id and nothing else...

Thoughts very much welcome.

[nick8325]

Unfortunately this doesn't work! Example:

prop_bad :: Int -> Property
prop_bad 3 = undefined
prop_bad _ = property True

ghci> quickCheck prop_bad
*** Failed! (after 59 tests):                            
Exception:
  Prelude.undefined
  CallStack (from HasCallStack):
    undefined, called at Test.hs:4:14 in main:Main

Note that QuickCheck fails to print the counterexample. The reason is that forAll works by generating a value, applying the property to it, and then modifying the returned Result so that it includes the generated value as part of the test case. But that last step can't happen if the property throws an exception. To make this work, forAll has to wrap the property in an exception handler.

Many QuickCheck combinators could have this problem, so the approach we ended up taking is to make property itself install the exception handler. That way, any combinator which is polymorphic in the property type (Testable prop => ...) automatically handles exceptions from its argument properties in the correct way. There's a comment about this here:

quickcheck/src/Test/QuickCheck/Property.hs

Lines 49 to 76 in d66336c

	-- The story for exception handling:
	--
	-- To avoid insanity, we have rules about which terms can throw
	-- exceptions when we evaluate them:
	-- * A rose tree must evaluate to WHNF without throwing an exception
	-- * The 'ok' component of a Result must evaluate to Just True or
	-- Just False or Nothing rather than raise an exception
	-- * IORose _ must never throw an exception when executed
	--
	-- Both rose trees and Results may loop when we evaluate them, though,
	-- so we have to be careful not to force them unnecessarily.
	--
	-- We also have to be careful when we use fmap or >>= in the Rose
	-- monad that the function we supply is total, or else use
	-- protectResults afterwards to install exception handlers. The
	-- mapResult function on Properties installs an exception handler for
	-- us, though.
	--
	-- Of course, the user is free to write "error "ha ha" :: Result" if
	-- they feel like it. We have to make sure that any user-supplied Rose
	-- Results or Results get wrapped in exception handlers, which we do by:
	-- * Making the 'property' function install an exception handler
	-- round its argument. This function always gets called in the
	-- right places, because all our Property-accepting functions are
	-- actually polymorphic over the Testable class so they have to
	-- call 'property'.
	-- * Installing an exception handler round a Result before we put it
	-- in a rose tree (the only place Results can end up).

[MaximilianAlgehed]

Isn't the solution here to only re-install the exception handler in the case where you go from something polymorphic to Property - that way we wouldn't have to re-apply the protection to something of type property?

[nick8325]

That would be reasonable, but it doesn't help in this case, does it? tabulate is polymorphic after all...

[MaximilianAlgehed]

Yes, so it would apply it the first time, but when tabulate is applied to something that is already of type property, we don't need to apply the protection again?

[nick8325]

Isn't that what your patch already does, though?

[MaximilianAlgehed]

I don't get it, did you run your counterexample above on this branch? Because I really cannot see how that would succeed on master but fail on this branch?

[nick8325]

Yep, on master I get a slightly different output - note the 3 at the end:

ghci> quickCheck prop_bad
*** Failed! (after 18 tests):                                            
Exception:
  Prelude.undefined
  CallStack (from HasCallStack):
    undefined, called at Test.hs:4:14 in main:Main
3

What's happening is that forAll is implemented roughly like this:

forAll gen prop = MkProperty $ do
   x <- gen
   unProperty $ counterexample (show x) $ prop x

and counterexample is polymorphic in the property type, so (on master) prop x gets wrapped in an exception handler, which is what allows counterexample to do its work. On your branch there's only an exception handler at the topmost level for this example. For the counterexample to be shown there needs to be an exception handler inside the call to counterexample.

[MaximilianAlgehed]

Right! But you only need one exception handler when you do counterexample . counterexample right?

[nick8325]

Yes that's true! But if it's counterexample . f . counterexample where f is a user-defined function, then you might need two (i.e. if f can crash). So you have to be able to distinguish these cases.

I have an idea how to do that, let me write it up...

[nick8325]

Right, here goes. Note that when I talk about "bottom" here, I really mean "crashing" - I've not thought about non-terminating properties.

Call a value of type Property "well-behaved" if it only ever generates non-bottom rose trees. More formally, if prop is well-behaved then in do { x <- unProperty prop; ...}, x is always non-bottom.

Note that any well-behaved Property does not need protecting. (In particular, we already maintain invariants that mean that a non-bottom rose tree must produce a non-bottom result.)

We'd like to maintain the invariant "every Property is well-behaved" but that's too strong (since the user can always pass in undefined :: Property). But, if we make Property an abstract type (i.e. hide MkProperty) then we can maintain the following invariant:

• every non-bottom Property is well-behaved.

Then we can make protecting a property a no-op as long as the property is non-bottom:

protectProperty :: Property -> Property
protectProperty p
  | crashes p = MkProperty (fmap protectProp (unProperty p)) -- in reality the result here is always a test case failure
  | otherwise = p
  where
     crashes :: a -> Bool
     crashes x = -- evaluate x to WHNF and return True if it throws an exception

The point is that if applying protectProperty twice in a row, the second call will be a no-op as the property will already be in WHNF.

[MaximilianAlgehed]

I like that idea a lot! I can try to implement this on the branch tomorrow - and I'll try to make a failing test of your "no counterexample" property too.

I've been thinking, wouldn't it be nice to write some QuickCheck properties to check the strictness properties of QuickCheck - one could have a little DSL that compiles to Property for which you could predict what the counterexamples should be and when things should fail because of exceptions etc.

[MaximilianAlgehed]

What I fail to understand here is why in your example the crashes p case doesn't just return MkProperty bottom because presumably unProperty bottom = bottom and fmap f bottom = bottom?

[nick8325]

Hmm, in this case I think (?) it works because fmap is in the Gen monad which is lazy (fmap f gen = MkGen (\g n -> f (unGen gen g n))). But I could be wrong :) In any case it's probably clearer to explicitly return a failing result there.

And yes, strictness properties would be very nice!

[MaximilianAlgehed]

Ah yes, in `Gen` you get `do x <- bottom; protectProp x = protectProp bottom` or something like that... Sincerely Maximilian Algehed, Ph.D.

…

On Wed, 25 Sept 2024 at 18:07, Nick Smallbone ***@***.***> wrote: Hmm, in this case I think (?) it works because fmap is in the Gen monad which is lazy (fmap f gen = MkGen (\g n -> f (unGen gen g n))). But I could be wrong :) In any case it's probably clearer to explicitly return a failing result there. And yes, strictness properties would be very nice! — Reply to this email directly, view it on GitHub <#415 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/ACBPPQPBU3KF5EWZOBQQ5PTZYLNVRAVCNFSM6AAAAABOTVRIASVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMZDGNZUGUYTINZZGU> . You are receiving this because you authored the thread.Message ID: ***@***.***>