Design of an Assertable refactoring of postcondition

[MaximilianAlgehed]

The postcondition interface does not give us a clean and easy way to give feedback about what went wrong in a postcondition. Instead you have to use the monitoring function for that - leading to repeated logic. That's a bit of a shame and a good approach to fixing this issue was identified in #11 but unfortunately due to some miscommunication that work has stalled for the moment. Hopefully we can pick that up again and use the good work that's there!

The idea is to use this issue to discuss the design of this refactoring here in a neutral manner that doesn't result in endless nit-picking of a PR.

[MaximilianAlgehed]

The wish-list for this extension is:

• The ability to add explanations for why a postcondition failed directly to the postconditon function without having to go through monitoring
• Backwards compatibility with postconditions that use Bool

The idea is to do something like:

data Assertion = Ok | Failed String deriving (Ord. Eq, Show)

class Assertable m a where
  assert :: a -> m Assertion

and

postcondition :: forall a r. Assertable m r => (state, state) -> Action state a -> LookUp m -> Realized m a -> r

[MaximilianAlgehed]

I've sketched this idea out on the branch PR-assertable but the solution isn't very nice. The problem is that you don't want forall r in the type of postcondition - you would like it to be forall a. exists r. ... but this can't be done without introducing extra types and crap. The solution might be to do something like RunModel m r state (or RunModel m assertions state). This isn't necessarily very nice :(

[MaximilianAlgehed]

@edsko any ideas for how we can get around this little wart?

[MaximilianAlgehed]

@abailly ☝️

[edsko]

My suggestion would be to drop the "must be backwards compatible" requirement. Then the closer analogy is I think QuickCheck's Testable class, where you have

class Testable a where
  property :: a -> Property

Then you could make Property quite a rich type, with associated operators; and if people just want to use Bool, they just need to write property (.. some boolean expression ..).

I think any of the alternatives are going to be a bit messy; as you point out, you'll need an additional parameter to the class (seems overkill). Wrapping it in some kind of existential wrapper won't help, because that will then immediately break the "backwards compatibility" requirement, in which case there are simpler solutions, I think.

[MaximilianAlgehed]

The problem I have with not doing the type parameter is that it means you have to write something like assert $ myPostcondition whenever your postcondition isn't of type m Assertion. That's not so nice :( If those are the options I think I prefer the extra type argument to RunModel.

[edsko]

Yes, it doesn't solve the type variable problem, you'd need to return Property. As for what it means, it would seem resaonable to me that I should be able to say something like forAll (elements ..) $ \x -> ... as my postcondition. This is how we specify properties of pure functions too, after all.

[MaximilianAlgehed]

What I wonder is whether the expected semantics of this lines up with what QuickCheck would do. As it stands we would end up picking only one element in the forAll each time the postcondition is evaluated. This might be ok, but it could also very easily result in flaky tests.

Seems like we have two decision points here:

• Assertable vs. Testable
• Type parameter in RunModel vs. rigid result in postcondition

I'm not sure what the right answer is to either question to be honest.

[abailly]

From a pure "client" point of view, the current situation does not seem very problematic to me: It would be great to have something better, but using monitoring to provide some feedback to the user or decorate the results is just fine. In other words, I (or rather we, in Hydra) don't have a need for a more generic solution so it's hard for me to decide on what this solution would be.
My suggestion: Let's wait for more feedback from actual usages of the library. If it turns out a couple more people are complaining about the current situation of postcondition then we can take those complaints into account and design a more general solution.

[edsko]

Testable versus Assertable I'm not totally sure about either. My vote would be for no type parameter, since I think it would be good to push users of the library towards a postcondition that actually gives a reason for the failure, and discourage the use of Bool.

But @abailly is right that it's not critical to fix. quickcheck-lockstep also works around it by evaluating (a generalization of) the postcondition in monitoring. I do think it would improve the user-friendliness of the library, though.

[MaximilianAlgehed]

I realised a major danger of using Testable instead of Assertable is that shrinking risks becoming flaky! QuickCheck re-generates nestled foralls when shrinking which will make shrinking flaky and unlikely to give you minimal counterexamples.

[edsko]

Ah. Yes, yes indeed. You are absolutely right sir, nested foralls should be avoided for sure. Ok, that's one design decision done :)

[MaximilianAlgehed]

@edsko and @abailly we found a nice design here. The version of qc-d on main now supports putting counterexample information directly in the postcondition definition via monitorPost. This reduces sharing and one could implement the ideas you had above @edsko nicely on top of this interface.