# QuickCheck / GADT

### From HaskellWiki

< QuickCheck (Difference between revisions)

DonStewart (Talk | contribs) m (move under idioms) |
|||

Line 277: | Line 277: | ||

</haskell> |
</haskell> |
||

+ | |||

+ | [[Category:Idioms]] |

## Revision as of 10:45, 22 May 2006

I couldn't find an example on how to use QuickCheck with GADTs. One solution is to use existential types. The example here is a solution to one of the exercises in Fun with Phantom Types. Note that here everything is heterogeneous and you may have defined your GADT to impose some constraints. In that case you will have to determine at which level you use existential types. For example, you could use them only at the top level.

## 1 Solution to Exercise

import Data.List import Data.Char import Test.QuickCheck import Control.Monad.State import Text.PrettyPrint data Dynamic = forall t . Dyn (Type t) t data Type :: * -> * where RInt :: Type Int RChar :: Type Char RList :: Type a -> Type [a] RPair :: Type a -> Type b -> Type (a,b) RDyn :: Type Dynamic rString :: Type String rString = RList RChar g = unfoldr f f n = Just (n `mod` 2, n `div` 2) compressInt x = take 32 (g x) compressChar x = take 7 (g ((ord x))) compress :: Type a -> a -> [Int] compress RInt x = compressInt x compress RChar x = compressChar x compress (RList t) [] = [0] compress (RList t) (x:xs) = 1:(compress t x ++ compress (RList t) xs) compress (RPair s t) (x,y) = compress s x ++ compress t y compress RDyn (Dyn t x) = compressRep (Rep t) ++ compress t x powersOf2 = 1:(map (2*) powersOf2) uncompressInt xs = sum (zipWith (*) xs powersOf2) uncompressChar x = chr (uncompressInt x) uncompress :: Type a -> [Int] -> a uncompress t x = let (r,_) = runState (bar t) x in r bar :: Type a -> State [Int] a bar RInt = do xs <- get let (ys,zs) = splitAt 32 xs put zs return (uncompressInt ys) bar RChar = do xs <- get let (ys,zs) = splitAt 7 xs put zs return (uncompressChar ys) bar (RList t) = do s <- get let (f,rs) = splitAt 1 s put rs if f == [0] then return [] else do x <- bar t xs <- bar (RList t) return (x:xs) bar (RPair s t) = do x <- bar s y <- bar t return (x,y) bar RDyn = do r <- baz case r of Rep s -> do t <- bar s return (Dyn s t) data Rep = forall t . Rep (Type t) compressRep :: Rep -> [Int] compressRep (Rep RInt) = [0,0,0] compressRep (Rep RChar) = [0,0,1] compressRep (Rep (RList t)) = 0:1:0:(compressRep (Rep t)) compressRep (Rep (RPair s t)) = 0:1:1:((compressRep (Rep s)) ++ (compressRep (Rep t))) compressRep (Rep RDyn) = [1,0,0] uncompressRep :: [Int] -> Rep uncompressRep xs = let (r,_) = runState baz xs in r baz :: State [Int] Rep baz = do s <- get case s of (0:0:0:xs) -> do put xs return (Rep RInt) (0:0:1:xs) -> do put xs return (Rep RChar) (0:1:0:xs) -> do put xs r <- baz case r of Rep x -> return (Rep (RList x)) (0:1:1:xs) -> do put xs r1 <- baz r2 <- baz case r1 of Rep x1 -> case r2 of Rep x2 -> return (Rep (RPair x1 x2)) (1:0:0:xs) -> do put xs return (Rep RDyn) instance Eq Rep where x == y = case x of Rep s -> case y of Rep t -> case s of RInt -> case t of RInt -> True otherwise -> False RChar -> case t of RChar -> True otherwise -> False RList r -> case t of RList q -> (Rep r) == (Rep q) otherwise -> False RPair r1 r2 -> case t of RPair q1 q2 -> ((Rep r1) == (Rep q1)) && ((Rep r2) == (Rep q2)) otherwise -> False RDyn -> case t of RDyn -> True otherwise -> False instance Show Rep where show x = render (prettyRep x) prettyRep x = case x of Rep s -> case s of RInt -> text "RInt" RChar -> text "RChar" RList y -> text "RList" <> space <> parens (prettyRep (Rep y)) RPair y1 y2 -> text "RPair" <> space <> parens (prettyRep (Rep y1)) <> space <> parens (prettyRep (Rep y2)) RDyn -> text "RDyn" instance Eq Dynamic where x == y = case x of Dyn s u -> case y of Dyn t v -> case s of RInt -> case t of RInt -> u == v otherwise -> False RChar -> case t of RChar -> u == v otherwise -> False RList r -> case t of RList q -> if (Rep r) == (Rep q) then (length u == length v) && (and (zipWith (\x y -> (Dyn r x) == (Dyn q y)) u v)) else False otherwise -> False RPair r1 r2 -> case t of RPair q1 q2 -> if ((Rep r1) == (Rep q1)) && ((Rep r2) == (Rep q2)) then ((Dyn r1 (fst u)) == (Dyn q1 (fst v))) && ((Dyn r2 (snd u)) == (Dyn q2 (snd v))) else False otherwise -> False RDyn -> case t of RDyn -> u == v otherwise -> False instance Show Dynamic where show x = render (prettyDyn x) pretty :: Type t -> t -> Doc pretty RInt i = int i pretty RChar c = quotes (char c) pretty (RList RChar) s = doubleQuotes (text s) pretty (RList ra) [] = text "[]" pretty (RList ra) (a:as) = text "[" <> pretty ra a <> prettyL as where prettyL [] = text "]" prettyL (a:as) = text "," <> pretty ra a <> prettyL as pretty (RPair ra rb) (a,b) = text "(" <> pretty ra a <> text "," <> pretty rb b <> text ")" pretty RDyn d = prettyDyn d prettyDyn :: Dynamic -> Doc prettyDyn x = case x of Dyn s u -> text "Dyn " <> parens (prettyRep (Rep s)) <> space <> pretty s u

## 2 QuickCheck Definitions

instance Arbitrary Char where arbitrary = oneof (map return ['A'..'z']) instance Arbitrary Rep where arbitrary = oneof [ return (Rep RInt), return (Rep RChar), do x <- arbitrary case x of (Rep t) -> return (Rep (RList t)), do x <- arbitrary y <- arbitrary case x of Rep t -> case y of Rep u -> return (Rep (RPair t u)) ] prop_IdemRep x = x == uncompressRep (compressRep x) where types = x::Rep instance Arbitrary Dynamic where arbitrary = sized dynamic' where dynamic' :: Int -> Gen Dynamic dynamic' 0 = oneof [ liftM (Dyn RInt) arbitrary, liftM (Dyn RChar) arbitrary ] dynamic' n | n > 0 = oneof [ liftM (Dyn RInt) arbitrary, liftM (Dyn RChar) arbitrary, sizedArbitraryList, liftM (Dyn (RPair RDyn RDyn)) (liftM2 (,) subdynamic subdynamic) ] where subdynamic = dynamic' (n `div` 2) sizedArbitraryList = do m <- arbitrary let q = m `mod` 10 liftM (Dyn (RList RDyn)) (sequence [subdynamic | i <- [0..q `asTypeOf` p]]) p :: Int p = undefined prop_IdemDyn x = x == uncompress RDyn (compress RDyn x) where types = x::Dynamic main = do quickCheck prop_IdemRep quickCheck prop_IdemDyn