Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

QuickCheck Gen is not a monad

Tags:

I have occasionally seen people say that the Gen type in QuickCheck does not obey the monad laws, though I have not seen much of an explanation to go with it. Now, QuickCheck 2.7's Test.QuickCheck.Gen.Unsafe module says Gen is only "morally" a monad, but the short explanation leaves me scratching my head. Can you give a step by step example of how Gen breaks the monad laws?

like image 262
Omari Norman Avatar asked Jun 30 '14 00:06

Omari Norman


People also ask

Is Gen A Monad?

QuickCheck Gen is not a monad.


1 Answers

If you want to prove something is a monad then you must prove that it satisfies the monad laws. Here's one

m >>= return = m

The documentation for Gen is referring to what the (=) in that law actually means. Gen values are functions, so it's difficult to compare them for equality. Instead, we might inline the definitions of (>>=) and return and prove via equational reasoning that the law holds

m       = m       >>= return
m       = m       >>= (\a -> MkGen (\_ _ -> a))
MkGen m = MkGen m >>= (\a -> MkGen (\_ _ -> a))
MkGen m = MkGen (\r n ->
                    let (r1,r2)  = split r
                        MkGen m' = (\a -> MkGen (\_ _ -> a)) (m r1 n)
                    in m' r2 n
                )
MkGen m = MkGen (\r n ->
                    let (r1,r2)  = split r
                        MkGen m' = MkGen (\_ _ -> m r1 n)
                    in m' r2 n
                )
MkGen m = MkGen (\r n ->
                    let (r1,r2)  = split r
                    in (\_ _ -> m r1 n) r2 n
                )
MkGen m = MkGen (\r n ->
                    let (r1,r2)  = split r
                    in m r1 n
                )
MkGen m = MkGen (\r -> m (fst $ split r))

So, ultimately, the monad law appears to fail to hold unless fst . split == id, which is doesn't. And shouldn't.

But morally, is fst (split r) the same as r? Well, so long as we're operating as though we're ignorant to the seed value then, yes, fst . split is morally equivalent to id. The actual values produced by Gen-as-a-function will vary, but the distribution of values is invariant.

And that's what the documentation is referring to. Our equality in the monad laws does not hold equationally, but instead only "morally" by considering Gen a to be a probability distribution over values of a.

like image 140
J. Abrahamson Avatar answered Oct 18 '22 11:10

J. Abrahamson