ANN: LeanCheck v0.9.0 -- enumerative property testing

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
10 messages Options
Reply | Threaded
Open this post in threaded view
|

ANN: LeanCheck v0.9.0 -- enumerative property testing

Rudy Matela

Hello Haskell Café,

A new version of LeanCheck is out (v0.9.0). LeanCheck is a property testing library (like QuickCheck) that tests values enumeratively.

Example. Here’s a simple example of LeanCheck in action showing that sorting is idempotent and list union is not commutative:

> import Test.LeanCheck
> import Data.List (sort, union)

> check $ \xs -> sort (sort xs) == sort (xs::[Int])
+++ OK, passed 200 tests.

> check $ \xs ys -> xs `union` ys == ys `union` (xs::[Int])
*** Failed! Falsifiable (after 4 tests):
[] [0,0]

LeanCheck works on all types that are instances of the Listable typeclass and is able to derive instances automatically using either Template Haskell or GHC.Generics. See LeanCheck’s Haddock documentation for more details.

Whats new? Version 0.9.0 marks the addition of Listable typeclass instances for most standard Haskell types defined in the Haskell 2010 Language Report. This means you’ll be able to test more functions without needing to define Listable instances yourself. LeanCheck’s changelog provides more details.

A separate package [leancheck-instances] provides instances for other types in the Haskell Platform.

Installing. You can find LeanCheck on Hackage or GitHub. It is also tracked on Stackage. As usual, you can install it with:

    $ cabal install leancheck

– Rudy


_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: ANN: LeanCheck v0.9.0 -- enumerative property testing

Arian van Putten
Awesome.  I always wondered what the pros/cons are compared to random testing like Quick check. When should I reach to enumerative testing?


On Thu, Jan 17, 2019, 03:11 Rudy Matela <[hidden email] wrote:

Hello Haskell Café,

A new version of LeanCheck is out (v0.9.0). LeanCheck is a property testing library (like QuickCheck) that tests values enumeratively.

Example. Here’s a simple example of LeanCheck in action showing that sorting is idempotent and list union is not commutative:

> import Test.LeanCheck
> import Data.List (sort, union)

> check $ \xs -> sort (sort xs) == sort (xs::[Int])
+++ OK, passed 200 tests.

> check $ \xs ys -> xs `union` ys == ys `union` (xs::[Int])
*** Failed! Falsifiable (after 4 tests):
[] [0,0]

LeanCheck works on all types that are instances of the Listable typeclass and is able to derive instances automatically using either Template Haskell or GHC.Generics. See LeanCheck’s Haddock documentation for more details.

Whats new? Version 0.9.0 marks the addition of Listable typeclass instances for most standard Haskell types defined in the Haskell 2010 Language Report. This means you’ll be able to test more functions without needing to define Listable instances yourself. LeanCheck’s changelog provides more details.

A separate package [leancheck-instances] provides instances for other types in the Haskell Platform.

Installing. You can find LeanCheck on Hackage or GitHub. It is also tracked on Stackage. As usual, you can install it with:

    $ cabal install leancheck

– Rudy

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: ANN: LeanCheck v0.9.0 -- enumerative property testing

Johannes Waldmann-2
In reply to this post by Rudy Matela
Yes, leancheck is awesome.


> When should I reach to enumerative testing?

I think enumerative testing
is best suited to algebraic data types.

https://mail.haskell.org/pipermail/haskell-cafe/2018-September/129951.html


In the past I had one standard example
where random enumeration seems better than enumerative:
(non)associativity of floating point ops
(I like to use this in teaching)


That's immediate in Quickcheck

quickCheck $ \ x y z -> (x::Double) + (y+z) == (x+y)+z
*** Failed! Falsifiable (after 3 tests and 3 shrinks):
-0.3
-1.4266097805446862
-1.2543117889178947


You don't get to see a counterexample in Smallcheck

Prelude Test.SmallCheck> smallCheck 5 $ \ x y z -> (x::Double) + (y+z)
== (x+y)+z
Completed 50653 tests without failure.


To my surprise, we now have

Prelude Test.LeanCheck> check $ \ x y z -> (x::Double) + (y+z) == (x+y)+z
*** Failed! Falsifiable (after 87 tests):
0.0 Infinity (-Infinity)


and I get the above (with "real" numbers) via

Prelude Test.LeanCheck> checkFor 1000 $ \ x y z -> isInfinite x ||
isInfinite y || isInfinite z || (x::Double) + (y+z) == (x+y)+z
*** Failed! Falsifiable (after 306 tests):
1.0 1.0 0.3333333333333333


Turns out the enumeration in Leancheck uses Rationals,
while Smallcheck uses  encodeFloat, which happens to
produce only "nice" numbers (very few bits set) in the beginning.

Prelude Test.LeanCheck> list 3 series :: [Double]
[0.0,1.0,-1.0,2.0,0.5,-2.0,4.0,0.25,-0.5,-4.0,-0.25]

Prelude Test.LeanCheck> take 12 $ list :: [Double]
[0.0,1.0,-1.0,Infinity,0.5,2.0,-Infinity,-0.5,-2.0,0.3333333333333333,3.0,-0.3333333333333333]


- J.W.


PS: this post wouldn't be complete without me complaining
that I cannot (easily) put the type annotation
where it belongs -  in the declaration of the name:

Prelude Test.LeanCheck> check $ \ (x::Double) y z -> x + (y+z) == (x+y)+z

<interactive>:22:12: error:
    Illegal type signature: ‘Double’
      Type signatures are only allowed in patterns with ScopedTypeVariables

Wat? TypeVariables? There aren't any!

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: ANN: LeanCheck v0.9.0 -- enumerative property testing

Johannes Waldmann-2
Sorry - I copy-pasted the prompt wrongly.
This is actually using Smallcheck:

> Prelude Test.LeanCheck> list 3 series :: [Double]
> [0.0,1.0,-1.0,2.0,0.5,-2.0,4.0,0.25,-0.5,-4.0,-0.25]

and this is Leancheck:

> Prelude Test.LeanCheck> take 12 $ list :: [Double]
> [0.0,1.0,-1.0,Infinity,0.5,2.0,-Infinity,-0.5,-2.0,0.3333333333333333,3.0,-0.3333333333333333]
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: ANN: LeanCheck v0.9.0 -- enumerative property testing

Rudy Matela
In reply to this post by Arian van Putten

Hi Arian,

When in doubt and with a bit of time to spare, you can always use both :-)

But here is some quick list of pros and cons:

  • LeanCheck/enumerative guarantees the smallest/simplest counterexample if one is found. This without the need of shrinking.

  • LeanCheck/enumerative allows for existential properties.

  • LeanCheck/enumerative guarantees that tests aren’t repeated most of the time.

  • QuickCheck/random always hits different test cases, so in the long run you may get more test coverage. With LeanCheck you only get more coverage when you configure more tests.

  • LeanCheck/enumerative is more memory intensive when compared to QuickCheck/random. With LeanCheck you may run out of memory when you’re running tens of millions of tests.

You can find more details here:

https://github.com/rudymatela/leancheck/blob/master/doc/faq.md#what-are-the-differences-between-quickcheck-and-leancheck

On Thu, Jan 17, 2019 at 10:57:17AM +0100, Arian van Putten wrote:

Awesome. I always wondered what the pros/cons are compared to random testing like Quick check. When should I reach to enumerative testing?


_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: ANN: LeanCheck v0.9.0 -- enumerative property testing

Rudy Matela
In reply to this post by Johannes Waldmann-2

On Thu, Jan 17, 2019 at 06:28:32PM +0100, Johannes Waldmann wrote:

Prelude Test.LeanCheck> checkFor 1000 $ \ x y z -> isInfinite x || isInfinite y || isInfinite z || (x::Double) + (y+z) == (x+y)+z *** Failed! Falsifiable (after 306 tests): 1.0 1.0 0.3333333333333333

Turns out the enumeration in Leancheck uses Rationals, while Smallcheck uses encodeFloat, which happens to produce only “nice” numbers (very few bits set) in the beginning.

I improved the LeanCheck floating enumeration starting with v0.8.0 to catch exactly this kind of error. :-)

PS: this post wouldn’t be complete without me complaining that I cannot (easily) put the type annotation where it belongs - in the declaration of the name:

Prelude Test.LeanCheck> check $ \ (x::Double) y z -> x + (y+z) == (x+y)+z

:22:12: error: Illegal type signature: ‘Double’ Type signatures are only allowed in patterns with ScopedTypeVariables

Wat? TypeVariables? There aren’t any!

You can get the above to parse by passing -XScopedTypeVariables to GHC:

$ ghci -XScopedTypeVariables
> import Test.LeanCheck
> check $ \(x::Double) y z -> x + (y+z) == (x+y) + z
*** Failed! Falsifiable (after 87 tests):
0.0 Infinity (-Infinity)

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: ANN: LeanCheck v0.9.0 -- enumerative property testing

Brandon Allbery
I think they're complaining about the name of the extension. Years ago, it was a separate extension, but it got folded into ScopedTypeVariables.

On Thu, Jan 17, 2019 at 8:01 PM Rudy Matela <[hidden email]> wrote:

On Thu, Jan 17, 2019 at 06:28:32PM +0100, Johannes Waldmann wrote:

Prelude Test.LeanCheck> checkFor 1000 $ \ x y z -> isInfinite x || isInfinite y || isInfinite z || (x::Double) + (y+z) == (x+y)+z *** Failed! Falsifiable (after 306 tests): 1.0 1.0 0.3333333333333333

Turns out the enumeration in Leancheck uses Rationals, while Smallcheck uses encodeFloat, which happens to produce only “nice” numbers (very few bits set) in the beginning.

I improved the LeanCheck floating enumeration starting with v0.8.0 to catch exactly this kind of error. :-)

PS: this post wouldn’t be complete without me complaining that I cannot (easily) put the type annotation where it belongs - in the declaration of the name:

Prelude Test.LeanCheck> check $ \ (x::Double) y z -> x + (y+z) == (x+y)+z

:22:12: error: Illegal type signature: ‘Double’ Type signatures are only allowed in patterns with ScopedTypeVariables

Wat? TypeVariables? There aren’t any!

You can get the above to parse by passing -XScopedTypeVariables to GHC:

$ ghci -XScopedTypeVariables
> import Test.LeanCheck
> check $ \(x::Double) y z -> x + (y+z) == (x+y) + z
*** Failed! Falsifiable (after 87 tests):
0.0 Infinity (-Infinity)
_______________________________________________
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.


--
brandon s allbery kf8nh

_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: ANN: LeanCheck v0.9.0 -- enumerative property testing

Johannes Waldmann-2
On 1/18/19 2:36 AM, Brandon Allbery wrote:
> I think they're complaining about the name of the extension.

Yes. And hat I need to use an extension at all - to be allowed
to annotate the declaration of an identifier with its type.

Of course it's easy to work around,
but I think it does not look good, especially when teaching.

- J.
_______________________________________________
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.
Reply | Threaded
Open this post in threaded view
|

Re: ANN: LeanCheck v0.9.0 -- enumerative property testing

Joachim Breitner-2
In reply to this post by Johannes Waldmann-2
Hi,


Am Donnerstag, den 17.01.2019, 18:28 +0100 schrieb Johannes Waldmann:
> <interactive>:22:12: error:
>     Illegal type signature: ‘Double’
>       Type signatures are only allowed in patterns with ScopedTypeVariables
>
> Wat? TypeVariables? There aren't any!

I feel your pain:
https://github.com/ghc-proposals/ghc-proposals/pull/119

Let’s hope we get Haskell2x somewhen, including (at least)
PatternSignatures, or even all of ScopedTypeVariables.

Interestingly, my proposal cites a rant from you from 10 years ago:
https://mail.haskell.org/pipermail/haskell-cafe/2009-April/059519.html
:-)

Cheers,
Joachim

--
Joachim Breitner
  [hidden email]
  http://www.joachim-breitner.de/


_______________________________________________
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.

signature.asc (849 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

Re: ANN: LeanCheck v0.9.0 -- enumerative property testing

Paul Brauner-3
Leancheck looks great! Could you also please compare it to feat? That's what I've been using for enumerating algebraic datatypes by size (vs depth) so far. 

On Fri, Jan 18, 2019, 16:22 Joachim Breitner <[hidden email] wrote:
Hi,


Am Donnerstag, den 17.01.2019, 18:28 +0100 schrieb Johannes Waldmann:
> <interactive>:22:12: error:
>     Illegal type signature: ‘Double’
>       Type signatures are only allowed in patterns with ScopedTypeVariables
>
> Wat? TypeVariables? There aren't any!

I feel your pain:
https://github.com/ghc-proposals/ghc-proposals/pull/119

Let’s hope we get Haskell2x somewhen, including (at least)
PatternSignatures, or even all of ScopedTypeVariables.

Interestingly, my proposal cites a rant from you from 10 years ago:
https://mail.haskell.org/pipermail/haskell-cafe/2009-April/059519.html
:-)

Cheers,
Joachim

--
Joachim Breitner
  [hidden email]
  http://www.joachim-breitner.de/

_______________________________________________
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.