2014-06-30 17 views
18

Ho visto occasionalmente persone dire che il tipo Gen in QuickCheck non obbedisce alle leggi della monade, anche se non ho visto molte spiegazioni per seguirlo. Ora, il modulo Test.QuickCheck.Gen.Unsafe di QuickCheck 2.7 dice che Gen è solo "moralmente" una monade, ma la breve spiegazione mi lascia grattarmi la testa. Puoi fare un esempio passo passo di come Gen rompe le leggi della monade?QuickCheck Gen non è una monade

+13

Codifica le leggi monade per 'Gen' come proprietà quickcheck, in esecuzione con lo stesso seme e lascia che quickcheck trovi i tuoi controesempi. :-) – luqui

risposta

25

Se vuoi dimostrare che qualcosa è una monade, devi dimostrare che soddisfa le leggi della monade. Ecco uno

m >>= return = m 

La documentazione per Gen si riferisce a ciò che il (=) in quella legge significa in realtà. I valori Gen sono funzioni, quindi è difficile confrontarli per l'uguaglianza. Invece, potremmo inline le definizioni di (>>=) e return e dimostrare attraverso il ragionamento equazionale che la legge vale

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

Quindi, in definitiva, la legge Monade sembra non riuscire a tenere a meno che fst . split == id, which is doesn't. E non dovrebbe

Ma moralmente, è fst (split r) lo stesso di r? Bene, a patto che stiamo operando come se ignorassimo il valore iniziale, sì, fst . split è moralmente equivalente a id. I valori effettivi prodotti da Gen -as-a-function variano, ma la distribuzione dei valori è invariabile.

E questo è ciò a cui si riferisce la documentazione. La nostra eguaglianza nelle leggi della monade non regge in modo equo, ma solo "moralmente" considerando Gen a una distribuzione di probabilità su valori di a.