haskell - near - Test.QuickCheck.Monadic: ¿por qué asert se aplica a Bool, no se puede probar a=> a

quick check near me

Question

En Prueba de código monádico con QuickCheck (Claessen, Hughes 2002) , assert tiene el tipo:

assert :: (Monad m, Testable a) => a -> PropertyM m ()

Sin embargo, en Test.QuickCheck.Monadic , tiene el tipo:

assert :: (Monad m) => Bool -> PropertyM m ()

¿Por qué assert tiene este último tipo en la biblioteca?

Answer 1

Creo que se debió a limitaciones técnicas, porque actualmente para evaluar una Testable con la Test.QuickCheck , necesita usar una de las funciones quickCheck* , que son muy centradas en IO . Esto sucede porque QuickCheck prueba Testable propiedades Testable al generar de forma aleatoria las posibles entradas (por defecto 100), tratando de encontrar un counterexample que demuestre que la propiedad es falsa. Si no se encuentra tal entrada, se asume que la propiedad es verdadera (aunque eso no es necesariamente la verdad; puede haber un contraejemplo que no se probó). Y para poder generar entradas aleatorias en Haskell, estamos atados a la mónada IO .

Tenga en cuenta que aunque la assert se definió de una manera tan genérica, se usa en todo el documento solo con Bool . Así que el autor de la biblioteca (el mismo del artículo) prefirió sacrificar el parámetro Testable genérico para un Bool simple, para no forzar ninguna mónada en este punto.

Y podemos ver que incluso han escrito la firma original como un comentario en el código fuente :

-- assert :: Testable prop => prop -> PropertyM m ()

También tenga en cuenta que a pesar del hecho de que la función de stop tiene una firma similar:

stop :: (Testable prop, Monad m) => prop -> PropertyM m a

No es lo mismo que la función de assert en el documento, ya que la primera detendrá el cálculo en ambos casos, ya sea que la condición sea True o False . Por otro lado, assert solo detendrá el cálculo si la condición es False :

⟦Afirmar Verdadero ≫ p⟧ = ⟦p⟧

⟦Afirmar Falso ≫ p⟧ = {retorno Falso}

Aunque podemos escribir fácilmente una versión IO de la función de assert del documento:

import Control.Monad
import Control.Monad.Trans
import Test.QuickCheck
import Test.QuickCheck.Monadic
import Test.QuickCheck.Property
import Test.QuickCheck.Test

assertIO :: Testable prop => prop -> PropertyM IO ()
assertIO p = do r <- liftIO $ quickCheckWithResult stdArgs{chatty = False} p
                unless (isSuccess r) $ fail "Assertion failed"

Y ahora podemos hacer una prueba para ver las diferencias entre assertIO y stop :

prop_assert :: Property
prop_assert = monadicIO $ do assertIO succeeded
                             assertIO failed

prop_stop :: Property
prop_stop = monadicIO $ do stop succeeded
                           stop failed

main :: IO ()
main = do putStrLn "prop_assert:"
          quickCheck prop_assert
          putStrLn "prop_stop:"
          quickCheck prop_stop

El succeeded y el failed podrían ser reemplazados por True y False , respectivamente. Era solo para demostrar que ahora no estamos limitados a Bool , en vez de eso, podemos usar cualquier Testable .

Y la salida es:

prop_assert
*** ¡Ha fallado! Afirmación fallida (después de 1 prueba):
prop_stop:
+++ OK, pasaron 100 pruebas.

Como podemos ver, a pesar del hecho de que el primer assertIO tuvo éxito, prop_assert falló debido al segundo assertIO . Por otro lado, prop_stop pasó la prueba, porque la primera stop tuvo éxito y el cálculo se detuvo en ese punto, sin probar la segunda stop .