QuickCheck: Come utilizzare checker esaustività per prevenire costruttori dimenticate di tipo somma

Question

Ho un tipo di dati Haskell come

data Mytype 
    = C1 
    | C2 Char 
    | C3 Int String 

Se io case su un Mytype e dimenticare di gestire uno dei casi, GHC mi dà un avviso (controllo di esaustività).

Ora voglio scrivere un esempio QuickCheck Arbitrary per generare MyTypes come:

instance Arbitrary Mytype where 
    arbitrary = do 
    n <- choose (1, 3 :: Int) 
    case n of 
     1 -> C1 
     2 -> C2 <$> arbitrary 
     3 -> C3 <$> arbitrary <*> someCustomGen 

Il problema di questo è che posso aggiungere una nuova alternativa a Mytype e dimenticare di aggiornare l'istanza arbitraria, quindi avere il mio i test non testano quell'alternativa.

Mi piacerebbe trovare un modo di utilizzare il controllo esaustivo di GHC per ricordarmi di casi dimenticati nella mia istanza arbitraria.

Il migliore che è venuta in mente è

arbitrary = do 
    x <- elements [C1, C2 undefined, C3 undefined undefined] 
    case x of 
    C1  -> C1 
    C2 _ -> C2 <$> arbitrary 
    C3 _ _ -> C3 <$> arbitrary <*> someCustomGen 

Ma in realtà non si sentono eleganti.

Mi sembra intuitivo che non ci sia una soluzione pulita al 100%, ma apprezzerei tutto ciò che riduce la possibilità di dimenticare questi casi, specialmente in un grande progetto in cui codice e test sono separati.

Answer 1

Qui utilizzo una variabile non utilizzata _x. Questo non è davvero più elegante della tua soluzione, però.

instance Arbitrary Mytype where 
    arbitrary = do 
    let _x = case _x of C1 -> _x ; C2 _ -> _x ; C3 _ _ -> _x 
    n <- choose (1, 3 :: Int) 
    case n of 
     1 -> C1 
     2 -> C2 <$> arbitrary 
     3 -> C3 <$> arbitrary <*> someCustomGen 

Naturalmente, si deve tenere l'ultimo case coerenti con la definizione di manichino _x, quindi non è completamente asciutto.

In alternativa, è possibile sfruttare Template Haskell per creare un asserzione in fase di compilazione, verificando che i costruttori in Data.Data.dataTypeOf siano quelli previsti. Questa affermazione deve essere mantenuta coerente con l'istanza Arbitrary, quindi anche questa non è completamente ASCIUTTA.

Se non avete bisogno di generatori personalizzati, credo Data.Data può essere sfruttata per generare Arbitrary istanze tramite Template Haskell (Credo di aver visto un po 'di codice di fare esattamente questo, ma non riesco a ricordare dove). In questo modo, non c'è alcuna possibilità che l'istanza possa perdere un costruttore.

Answer 2

Ho implementato una soluzione con TemplateHaskell, è possibile trovare un prototipo a https://gist.github.com/nh2/d982e2ca4280a03364a8. Con questo si può scrivere:

instance Arbitrary Mytype where 
    arbitrary = oneof $(exhaustivenessCheck ''Mytype [| 
     [ pure C1 
     , C2 <$> arbitrary 
     , C3 <$> arbitrary <*> arbitrary 
     ] 
    |]) 

Funziona così: Si dà un nome tipo (come ''Mytype) ed espressione (nel mio caso un elenco di arbitrary stile Gen s). Ottiene l'elenco di tutti i costruttori per quel tipo di nome e controlla se l'espressione contiene tutti questi costruttori almeno una volta. Se hai appena aggiunto un costruttore ma hai dimenticato di aggiungerlo all'istanza Arbitrary, questa funzione ti avviserà al momento della compilazione.

Questo è come è implementato con TH:

exhaustivenessCheck :: Name -> Q Exp -> Q Exp 
exhaustivenessCheck tyName qList = do 
    tyInfo <- reify tyName 
    let conNames = case tyInfo of 
     TyConI (DataD _cxt _name _tyVarBndrs cons _derives) -> map conNameOf cons 
     _ -> fail "exhaustivenessCheck: Can only handle simple data declarations" 

    list <- qList 
    case list of 
    input@(ListE l) -> do 
     -- We could be more specific by searching for `ConE`s in `l` 
     let cons = toListOf tinplate l :: [Name] 
     case filter (`notElem` cons) conNames of 
     [] -> return input 
     missings -> fail $ "exhaustivenessCheck: missing case: " ++ show missings 
    _ -> fail "exhaustivenessCheck: argument must be a list" 

sto usando GHC.Generics per attraversare con facilità l'albero sintassi del Exp: Con toListOf tinplate exp :: [Name] (da lens) posso facilmente trovare tutti Name s in tutta la exp.

Mi ha sorpreso che i tipi di Language.Haskell.TH non hanno Generic casi, e nessuno dei due (con corrente GHC 7.8) fanno Integer o Word8 - Generic istanze per questi sono necessari perché appaiono in Exp. Quindi li ho aggiunti come istanze orfane (per la maggior parte delle cose, StandaloneDeriving lo fa ma per i tipi primitivi come Integer ho dovuto copiare e incollare istanze come Int li ha).

La soluzione non è perfetta perché non utilizza il controllo di esaustività come case, ma come d'accordo, ciò non è possibile mentre si rimane ASCIUTTI, e questa soluzione TH è ASCIUTTA.

Un possibile miglioramento/alternativa sarebbe scrivere una funzione TH che controlli questo per tutte le istanze Arbitrarie in un intero modulo contemporaneamente invece di chiamare exhaustivenessCheck all'interno di ciascuna istanza Arbitraria.

Answer 3

Si desidera garantire che il codice si comporti in un modo particolare; il modo più semplice per verificare il comportamento del codice è testarlo.

In questo caso, il comportamento desiderato è che ogni costruttore ottiene una copertura ragionevole nei test. Possiamo controllare che con un semplice test:

allCons xs = length xs > 100 ==> length constructors == 3 
      where constructors = nubBy eqCons xs 
        eqCons C1  C1  = True 
        eqCons C1  _  = False 
        eqCons (C2 _) (C2 _) = True 
        eqCons (C2 _) _  = False 
        eqCons (C3 _ _) (C3 _ _) = True 
        eqCons (C3 _ _) _  = False 

questo è abbastanza ingenuo, ma è un buon primo colpo. I suoi vantaggi:

• eqCons attiverà un esaustività avviso se vengono aggiunti nuovi costruttori, che è ciò che si desidera
• Verifica che l'istanza sta gestendo tutti i costruttori, che è ciò che si desidera
• E anche controlla che tutti i costruttori sono in realtà generati con una certa probabilità utile (in questo caso almeno l'1%)
• E anche verifica che l'istanza è utilizzabile, ad esempio, . non appendere

I suoi svantaggi:

• richiede una grande quantità di dati di test, al fine di filtrare quelli con lunghezza> 100
• eqCons è abbastanza prolisso, dal momento che un catch-all eqCons _ _ = False avrebbe bypassare verificare l'esaustività
• utilizza i numeri magici 100 e 3
• Non molto generico

Ci sono modi per migliorare questo, ad es. possiamo calcolare i costruttori usando i dati.Modulo dati:

allCons xs = sufficient ==> length constructors == consCount 
      where sufficient = length xs > 100 * consCount 
        constructors = length . nub . map toConstr $ xs 
        consCount = dataTypeConstrs (head xs) 

Questa perde il controllo di completezza di compilazione, ma è ridondante fintanto che ci prova con regolarità e il nostro codice è diventato più generico.

Se vogliamo davvero il controllo di completezza, ci sono alcuni posti dove abbiamo potuto calzascarpe indietro in:

allCons xs = sufficient ==> length constructors == consCount 
      where sufficient = length xs > 100 * consCount 
        constructors = length . nub . map toConstr $ xs 
        consCount = length . dataTypeConstrs $ case head xs of 
                    x@(C1)  -> x 
                    x@(C2 _) -> x 
                    x@(C3 _ _) -> x 

Si noti che usiamo consCount per eliminare la magia 3 completamente. La magia 100 (che ha determinato la frequenza minima richiesta di un costruttore) ora viene ridimensionata con consCount, ma ciò richiede solo ancora più dati di test!

Possiamo risolvere che molto facilmente utilizzando un newtype:

consCount = length (dataTypeConstrs C1) 

newtype MyTypeList = MTL [MyType] deriving (Eq,Show) 

instance Arbitrary MyTypeList where 
    arbitrary = MTL <$> vectorOf (100 * consCount) arbitrary 
    shrink (MTL xs) = MTL (shrink <$> xs) 

allCons (MTL xs) = length constructors == consCount 
        where constructors = length . nub . map toConstr $ xs 

Possiamo mettere un semplice controllo esaustività lì da qualche parte, se ci piace, per esempio.

instance Arbitrary MyTypeList where 
    arbitrary = do x <- arbitrary 
       MTL <$> vectorOf (100 * consCount) getT 
       where getT = do x <- arbitrary 
           return $ case x of 
              C1  -> x 
              C2 _ -> x 
              C3 _ _ -> x 
    shrink (MTL xs) = MTL (shrink <$> xs)