Testing monadic laws using QuickCheck

2019-07-04 02:36发布

问题:

Is there a library or tools for testing the laws of a custom monad? My current hacked attempt goes something like this:

  • Define Arbitrary1, similar to Eq1, Show1 etc.
  • Define a helper type that wraps Arbitrary1 as Arbitrary.
  • Define a test (for example) for monadic laws.

Is any of this already implemented somewhere?


{-# LANGUAGE RankNTypes, ScopedTypeVariables #-}
import Data.Functor.Classes
import Data.Proxy
import Test.QuickCheck
import Test.QuickCheck.Function
import Test.QuickCheck.Poly

Define Arbitrary1 for * -> * types:

class Arbitrary1 m where
    arbitrary1 :: (Arbitrary a) => Gen (m a)
    shrink1 :: (Arbitrary a) => m a -> [m a]
    shrink1 _ = []

And a helper wrapper so that we can use functions that work with Arbitrary:

newtype Action m a = Action { getAction :: m a }

instance (Arbitrary a, Arbitrary1 m) => Arbitrary (Action m a) where
    arbitrary = Action <$> arbitrary1
    shrink = map Action . shrink1 . getAction

instance (Show a, Show1 m) => Show (Action m a) where
    showsPrec p = showsPrec1 p . getAction

Now we can write a test like this:

-- (m >>= f) >>= g  ≡   m >>= (\x -> f x >>= g)
testBindAssoc :: forall m . (Monad m, Arbitrary1 m, Show1 m, Eq1 m) => Proxy m -> Property
testBindAssoc _ =
    forAllShrink (arbitrary :: Gen (Action m A)) shrink $ \m' ->
    forAllShrink (arbitrary :: Gen (Fun A (Action m B))) shrink $ \f' ->
    forAllShrink (arbitrary :: Gen (Fun B (Action m C))) shrink $ \g' ->
    let m = getAction m'
        f = getAction <$> apply f'
        g = getAction <$> apply g'
        k = (m >>= f) >>= g
        l = m >>= (\x -> f x >>= g)
    in counterexample (showsPrec1 0 k . showString " != " . showsPrec1 0 l $ "")
        $ k `eq1` l

And let's write a broken Writer monad:

{-# LANGUAGE GeneralizedNewtypeDeriving #-}
import Control.Monad.Writer

newtype MyMonad w a = MyMonad { runMyMonad :: Writer w a }
  deriving (Functor, Applicative)

instance (Monoid w) => Monad (MyMonad w) where
    return = pure
    k >>= f = let (a, w) = runWriter . runMyMonad $ k
              in MyMonad $ writer (a, w <> w) >>= (runMyMonad . f)
--                                    ^ broken here

getMyMonad :: MyMonad w a -> (a, w)
getMyMonad = runWriter . runMyMonad

instance (Eq w) => Eq1 (MyMonad w) where
    eq1 k l = getMyMonad k == getMyMonad l

instance (Show w) => Show1 (MyMonad w) where
    showsPrec1 p k = showsPrec p (getMyMonad k)

instance (Monoid w, Arbitrary w) => Arbitrary1 (MyMonad w) where
    arbitrary1 = MyMonad . writer <$> arbitrary
    shrink1 = map (MyMonad . writer) . shrink . getMyMonad

main :: IO ()
main = quickCheck (testBindAssoc (Proxy :: Proxy (MyMonad (Sum Int))))

Fails with:

*** Failed! Falsifiable (after 2 tests and 13 shrinks):   
(1,Sum {getSum = 1})
{_->(1,Sum {getSum = 0})}
{_->(1,Sum {getSum = 0})}
(1,Sum {getSum = 4}) != (1,Sum {getSum = 2})

Any ideas for improvements?