QuickCheck / GADT
Jump to navigation
Jump to search
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.
Solution to exercise
{-#
OPTIONS_GHC
-XExistentialQuantification
-XGADTs
#-}
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
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