Personal tools

QuickCheck / GADT

From HaskellWiki

< QuickCheck
Revision as of 08:01, 30 November 2008 by Dominic (Talk | contribs)

Jump to: navigation, 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.


1 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

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