Testy QuickCheck dla typów zależnych

Question

Piszę Vector i Matrix typów danych, które są zależnie wpisane.

data Vector n e where 
    EmptyVector :: Vector Zero e 
    (:>)  :: e -> Vector n e -> Vector (Succ n) e 

deriving instance Eq e => Eq (Vector n e) 

infixr :> 

data Matrix r c e where 
    EmptyMatrix :: Matrix Zero c e 
    (:/)  :: Vector c e -> Matrix r c e -> Matrix (Succ r) c e 

deriving instance Eq e => Eq (Matrix r c e) 

infixr :/ 

Są zależne od liczb naturalnych, również typu.

data Natural where 
    Zero :: Natural 
    Succ :: Natural -> Natural 

Napisałem funkcję do obliczania liczby kolumn w macierzy.

columns :: Matrix r c e -> Int 
columns m = Fold.foldr (\_ n -> 1 + n) 0 $ getRow 0 m 

getRow :: Int -> Matrix r c e -> Vector c e 
getRow 0 (v :/ _) = v 
getRow i (_ :/ m) = getRow (i - 1) m 
getRow _ EmptyMatrix = error "Cannot getRow from EmptyMatrix." 

Chciałbym teraz chcesz przetestować funkcję columns użyciu QuickCheck.

Aby to zrobić, muszę zadeklarować Matrix i Vector jako wystąpienia klasy typu Arbitrary dostarczone przez QuickCheck.

Jednak nie mam pojęcia, jak to zrobić.

• Czy fakt, że moje dane są zależnie wpisane wpływa na to, w jaki sposób piszę te wystąpienia?

• Jak wygenerować macierze o dowolnej długości, upewniając się, że pasują do ich definicji (np. (Succ (Succ r)) będą miały dwa wiersze)?

Answer 1

możesz napisać instancji przez pewien okres znany w czasie kompilacji:

instance Arbitrary (Vector Zero e) where 
    arbitrary = return EmptyVector 

instance (Arbitrary e, Arbitrary (Vector n e)) 
    => Arbitrary (Vector (Succ n) e) where 
    arbitrary = do 
     e <- arbitrary 
     es <- arbitrary 
     return (e :> es) 

same powyższe przypadki nie są bardzo przydatne, chyba że chcesz napisać jeden wyraz dla każdego długość, którą chcesz wypróbować (lub pobierz szablon-haskell do wygeneruj te wyrażenia). Jednym ze sposobów, aby uzyskać Int zdecydować, co rodzaj n powinno być to, aby ukryć n w egzystencjalnym:

data BoxM e where 
    BoxM :: Arbitrary (Vector c e) => Matrix r c e -> BoxM e 

data Box e where Box :: Arbitrary (Vector c e) => Vector c e -> Box e 

addRow :: Gen e -> BoxM e -> Gen (BoxM e) 
addRow mkE (BoxM es) = do 
    e <- mkE 
    return $ BoxM (e :/ es) 

firstRow :: Arbitrary a => [a] -> BoxM a 
firstRow es = case foldr (\e (Box es) -> Box (e :> es)) (Box EmptyVector) es of 
    Box v -> BoxM (v :/ EmptyMatrix) 

Z addRow i firstRow, powinno być dość proste napisać mkBoxM :: Int -> Int -> Gen (BoxM Int), a następnie użyć to:

forAll (choose (0,3)) $ \n -> forAll (choose (0,3)) $ \m -> do 
     BoxM matrix <- mkBoxM n m 
     return $ columns matrix == m -- or whatever actually makes sense