QuickCheck Gen is not a monad
Asked Answered
F

1

22

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?

Fossilize answered 30/6, 2014 at 0:50 Comment(1)
Encode the monad laws for Gen as quickcheck properties, running with the same seed, and let quickcheck find your counterexamples. :-)Vance
S
28

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.

Snuffy answered 30/6, 2014 at 1:16 Comment(0)

© 2022 - 2024 — McMap. All rights reserved.