Я иногда видел, как люди говорят, что тип Gen в QuickCheck не подчиняется законам монады, хотя я не видел много объяснений, чтобы пойти с ним. Теперь QuickCheck 2.7 Модуль Test.QuickCheck.Gen.Unsafe говорит, что Gen является только "морально" монадой, но краткое объяснение оставляет меня царапающей мою голову, Можете ли вы дать пошаговый пример того, как Gen нарушает законы монады?
QuickCheck Gen не является монадой
Ответ 1
Если вы хотите доказать, что что-то есть монада, тогда вы должны доказать, что оно удовлетворяет законам монады. Здесь один
m >>= return = m
Документация для Gen относится к тому, что на самом деле означает (=) в этом законе. Значения Gen - это функции, поэтому их трудно сравнивать для равенства. Вместо этого мы могли бы установить определения (>>=) и return и доказать с помощью эквациональных рассуждений, что закон имеет место
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))
Итак, в конечном счете, закон монады, похоже, не удерживается, если fst . split == id, который не соответствует. И не должно.
Но морально, fst (split r) то же самое, что и r? Ну, пока мы работаем так, как будто мы не знаем начального значения, да, fst . split морально эквивалентен id. Фактические значения, выражаемые функцией Gen -а-a-функции, будут меняться, но распределение значений инвариантно.
И это то, о чем идет речь в документации. Наше равенство в законах монады не выполняется равномерно, а вместо этого "морально", рассматривая Gen a как распределение вероятности по значениям a.