haskell - las - monadas leibniz

QuickCheck Gen no es una mónada

Question

Ocasionalmente he visto a personas decir que el tipo Gen en QuickCheck no obedece las leyes de la mónada, aunque no he visto muchas explicaciones que lo acompañen. Ahora, el módulo Test.QuickCheck.Gen.Unsafe QuickCheck 2.7 dice que Gen es solo una mónada "moralmente", pero la breve explicación me deja rascándome la cabeza. ¿Puede dar un ejemplo paso a paso de cómo Gen infringe las leyes de la mónada?

Answer 1

Si desea probar que algo es una mónada, debe probar que cumple con las leyes de la mónada. Aquí hay uno

m >>= return = m

La documentación para Gen se refiere a lo que realmente significa (=) en esa ley. Gen valores Gen son funciones, por lo que es difícil compararlos para la igualdad. En su lugar, podríamos incluir las definiciones de (>>=) y return y probarlas mediante el razonamiento ecuacional que sostiene la ley.

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

Entonces, en última instancia, la ley de la mónada parece fallar a menos que fst . split == id fst . split == id , que no lo es . Y no debería.

Pero moralmente, ¿es fst (split r) lo mismo que r ? Bueno, mientras estemos operando como si fuéramos ignorantes del valor semilla entonces, sí, fst . split fst . split es moralmente equivalente a id . Los valores reales producidos por Gen -as-a-function variarán, pero la distribución de valores es invariante.

Y a eso se refiere la documentación. Nuestra igualdad en las leyes de la mónada no se sostiene de manera ecuatorial, sino que solo "moralmente" al considerar que Gen a a es una distribución de probabilidad sobre los valores de a .