QuickCheck Gen ist kein Monad

Question

Ich habe gelegentlich Leute sagen, dass die Gen-Typ in QuickCheck nicht den Monaden Gesetzen gehorchen, obwohl ich nicht viel von einer Erklärung gesehen habe, um damit zu gehen. Nun, QuickCheck 2.7's Test.QuickCheck.Gen.Unsafe Modul sagt Gen ist nur "moralisch" eine Monade, aber die kurze Erklärung lässt mich am Kopf kratzen. Können Sie Schritt für Schritt Beispiele dafür geben, wie Gen die Monadengesetze bricht?

Answer 1

Wenn Sie beweisen wollen, dass etwas eine Monade ist, dann müssen Sie beweisen, dass es die Monadengesetze erfüllt. Hier ist eine

m >>= return = m 

Die Dokumentation für Gen bezieht sich auf das, was die (=) in diesem Gesetz eigentlich bedeutet. Gen Werte sind Funktionen, daher ist es schwierig, sie auf Gleichheit zu prüfen. Stattdessen könnten wir die Definitionen von (>>=) und return und beweisen über equational Argumentation inline, dass das Gesetz

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

hält also letztlich erscheint die Monade Gesetz zu scheitern, es sei denn fst . split == id, which is doesn't zu halten. Und sollte nicht.

Aber moralisch ist fst (split r) das gleiche wie r? Nun, solange wir so arbeiten, als ob wir den Seed-Wert nicht kennen, dann ist fst . split moralisch gleichwertig zu id. Die tatsächlichen Werte, die von Gen -als-eine-Funktion erzeugt werden, werden variieren, aber die Verteilung der Werte ist invariant.

Und darauf bezieht sich die Dokumentation. Unsere Gleichheit in den Monadengesetzen gilt nicht gleichsinnig, sondern nur "moralisch", indem wir Gen a als Wahrscheinlichkeitsverteilung über die Werte a betrachten.