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?
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
.
© 2022 - 2024 — McMap. All rights reserved.
Gen
as quickcheck properties, running with the same seed, and let quickcheck find your counterexamples. :-) – Vance