Ответ 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.