Блог

Я иногда видел, как люди говорили, что тип Gen в QuickCheck не подчиняется законам монады, хотя я не видел большого объяснения этому. Теперь модуль QuickCheck 2.7 Test.QuickCheck.Gen.Unsafe говорит, что Gen является только «морально» монадой, но краткое объяснение заставляет меня почесать голову. Можете ли вы привести пошаговый пример того, как Gen нарушает законы монады?

Если вы хотите доказать, что что-то является монадой, вы должны доказать, что оно удовлетворяет законам монады. Вот один

 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 как функция, будут меняться, но распределение значений остается неизменным.

И это то, на что ссылается документация. Наше равенство в законах монад выполняется не равномерно, а вместо этого только «морально», считая Gen a распределение вероятностей по значениям a .