[Haskell-cafe] property testing with context

[Ben Franksen]

Hi Ollie

This is fantastic! It's certainly much more than I hoped for.

I haven't looked into the details of your plugin yet, but from your
description it looks as if this is currently geared towards "classical"
unit tests. Perhaps this is not a problem: I think quickcheck & co
report exceptions as a failed property, and if they don't we'll just
have to catch the exception, print it and return False.

I will definitely try it out and report back.

Cheers
Ben

Am 19.10.2018 um 23:25 schrieb Oliver Charles:
> Perhaps the work in my "assert-explainer" project is relevant here -
> https://github.com/ocharles/assert-explainer.
> 
> The idea is your tests should just be writing "assert
> someArbitraryExpressionEvaluatingToBool", and then having some
> compiler magic recover the context for you when it goes wrong. To cite
> my own README:
> 
> 
> You write:
> 
>     assert (length xs == 4)
> 
> No need for lots of special assertEqual etc functions.
> 
> When the assertion fails, you will get much more context:
> 
> ✘ Assertion failed!
>     length xs == 4 /= True (at Test.hs:18:12-25)
> 
>   I found the following sub-expressions:
>     - length xs = 3
>     - xs = [1,2,3]
> 
> 
> This is done via a GHC source plugin that rewrites "assert (length xs
> == 4)" into an expression that - if False - prints much more
> information.
> 
> It's very early days for this plugin, but the goal is to reach parity
> with https://docs.pytest.org/en/latest/example/reportingdemo.html#tbreportdemo.
> 
> Hope this helps,
> Ollie
> On Fri, Oct 19, 2018 at 8:20 AM Ben Franksen <ben.franksen at online.de> wrote:
>>
>> Hi everyone
>>
>> it seems to be the season for new variations on the "property testing"
>> theme, so I would like to chime in... not to announce a new library,
>> sadly, but with a rough idea how the existing ones could perhaps be
>> improved, based on practical experience in Darcs.
>>
>> The problem I have is that there is a tension between
>>
>> (a) stating a property in a clear and simple way, so its code doubles as
>> a formal specification
>>
>> and
>>
>> (b) writing the property in such a way that when it fails, the reported
>> value(s) give enough information about the context to be useful for
>> finding the cause of the problem.
>>
>> Let me give an example to demonstrate what I mean.
>>
>> There is a simple law that says if a sequential pair of patches A;B
>> commutes to B';A' then B';A' commutes back to A;B. In code this looks
>> (more or less) like this:
>>
>> prop_recommute :: Commute p => (p :> p) wA wB -> Bool
>> prop_recommute (x:>y)
>>   | Just (y':>x') <- commute (x:>y) =
>>       case commute (y':>x')of
>>         Just (x'':>y'') -> x==x'' && y==y''
>>         Nothing -> False
>>   | otherwise = True
>>
>> This is a bit more verbose than the informal spec but still quite readable.
>>
>> Now suppose this property fails. So quickcheck reports the counter
>> example pair (X:>Y) for some X and Y. But that isn't too useful in
>> itself. We'd like to know a bit more:
>>
>>  * did the second commute fail?
>>  * or did it succeed but x/=x'' or y/=y''?
>>  * and in the latter case, which of the two?
>>
>> So in practice our property code looks more like this:
>>
>> prop_recommute :: (ShowPatch p, Commute p) => (p :> p) wA wB -> Bool
>> prop_recommute (x :> y)
>>   | Just (y' :> x') <- commute (x :> y) =
>>       case commute (y' :> x') of
>>         Nothing ->
>>           failed (redText "failed, where x" $$ displayPatch x $$
>>                   redText ":> y" $$ displayPatch y $$
>>                   redText "y'" $$ displayPatch y' $$
>>                   redText ":> x'" $$ displayPatch x')
>>         Just (x'' :> y'') ->
>>           if y'' /= y
>>             then
>>               failed (redText "y'' =/\\= y failed, where x" $$
>>                       displayPatch x $$
>>                       redText ":> y" $$ displayPatch y $$
>>                       redText "y'" $$ displayPatch y' $$
>>                       redText ":> x'" $$ displayPatch x' $$
>>                       redText "x''" $$ displayPatch x'' $$
>>                       redText ":> y''" $$ displayPatch y'')
>>             else
>>               if x'' /= x
>>                 then
>>                   failed (redText "x'' /= x, where x" $$
>>                           displayPatch x $$
>>                           redText ":> y" $$ displayPatch y $$
>>                           redText "y'" $$ displayPatch y' $$
>>                           redText ":> x'" $$ displayPatch x' $$
>>                           redText "x''" $$ displayPatch x'' $$
>>                           redText ":> y''" $$ displayPatch y'')
>>                 else True
>>   | otherwise = True
>>
>> Now this code tells us exactly what went wrong when the property fails
>> but it is ugly and repetitive and the additional code obscures the
>> simple logical content. So this is no longer quite as suitable for a
>> (human readable) formal spec.
>>
>> I wonder if displaying
>>
>> (1) all relevant contextual variables and
>> (2) "where in the code it fails"
>>
>> could be automated away, somehow. I guess this is not trivial and may
>> require syntactic analysis, so perhaps expecting a /library/ to solve
>> the problem is unrealistic, except perhaps by using Template Haskell.
>> I'd also go with a separate tool that extracts properties from a module
>> and enriches them with code that displays the additional information.
>>
>> Tackling this problem might be an interesting theme for a master
>> thesis... ;-)
>>
>> Cheers
>> Ben
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> To (un)subscribe, modify options or view archives go to:
>> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
>> Only members subscribed via the mailman list are allowed to post.
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
>