QuickCheck Gen nie jest monadą

Question

Od czasu do czasu widzę ludzi, którzy mówią, że typ Gen w QuickCheck nie przestrzega praw monady, chociaż nie widziałem zbyt wiele wyjaśnień, aby z nim poradzić. Teraz moduł QuickCheck 2.7, Test.QuickCheck.Gen.Unsafe mówi, że Gen jest tylko "moralnie" monadą, ale krótkie wyjaśnienie pozostawia mi drapanie w głowę. Czy możesz podać krok po kroku, jak Gen łamie prawa Monady?

Answer 1

Jeśli chcesz udowodnić, że coś jest monadą, musisz udowodnić, że spełnia ona prawa monad. Oto jeden

m >>= return = m 

Dokumentacja Gen odnosi się do tego, co (=) w tej ustawie w rzeczywistości oznacza. Gen wartości są funkcjami, więc trudno jest je porównać dla równości. Zamiast tego, możemy inline definicje (>>=) i return i udowodnić poprzez equational rozumowania, że ​​prawo posiada

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)) 

Więc ostatecznie ustawa monada wydaje się nie trzymać, chyba fst . split == id, which is doesn't. I nie powinien.

Ale moralnie, czy fst (split r) jest takie samo jak r? Cóż, dopóki działamy tak, jakbyśmy nie mieli pojęcia o wartości nasion, tak, tak, fst . split jest moralnie równoważne z id. Rzeczywiste wartości generowane przez Gen -as-a-function będą się różnić, ale rozkład wartości jest niezmienny.

I do tego odnosi się dokumentacja. Nasza równość w prawach monad nie ma charakteru równania, ale zamiast tego jest "moralnie" biorąc pod uwagę, że Gen a jest rozkładem prawdopodobieństwa nad wartościami a.