Module documentation for 0.1.3
Express is a library for manipulating dynamically typed Haskell expressions.
Data.Dynamic but with support for encoding applications and
To install the latest Express version from Hackage, just run:
$ cabal update $ cabal install express
> import Data.Express
> let false = val False > :t false false :: Expr > print false False :: Bool > let one = val (1 :: Int) > :t one one :: Expr > print one 1 :: Int
> let notE = value "not" not > :t notE notE :: Expr > print notE not :: Bool -> Bool
> let notFalse = notE :$ false > :t notFalse notFalse :: Expr > notFalse not False :: Bool
> evaluate notFalse :: Maybe Bool Just True > evaluate notFalse :: Maybe Int Nothing > eval False notFalse True > eval (0::Int) notFalse 0
Example 1: heterogeneous lists
Data.Dynamic, we can use Express to create heterogeneous lists.
Here, we use applications of
val to create a heterogeneous list:
> let xs = [val False, val True, val (1::Int), val (2::Int), val (3::Integer), val "123"] > :t xs xs :: [Expr] > xs [ False :: Bool , True :: Bool , 1 :: Int , 2 :: Int , 3 :: Integer , "123" :: [Char] ]
We can then apply
evaluate to select values of different types:
> import Data.Maybe > mapMaybe evaluate xs :: [Bool] [False,True] > mapMaybe evaluate xs :: [Int] [1,2] > mapMaybe evaluate xs :: [Integer]  > mapMaybe evaluate xs :: [String] ["123"]
Example 2: listing applications
Carrying on from Example 1, we define an heterogeneous list of functions
> let fs = [value "not" not, value "&&" (&&), value "abs" (abs :: Int -> Int)] > :t fs fs :: [Expr]
$$ we list the type correct applications of functions in
> catMaybes [f $$ x | f <- fs, x <- xs] [ not False :: Bool , not True :: Bool , (False &&) :: Bool -> Bool , (True &&) :: Bool -> Bool , abs 1 :: Int , abs 2 :: Int ]
Example 3: u-Extrapolate
u-Extrapolate is a property-based testing library capable of generalizing counter-examples. It’s implementation has under 40 lines of code. Besides, using Express to encode expressions, it uses LeanCheck for generating test values.
import Data.Express import Test.LeanCheck hiding (counterExample, check)
Given a maximum number of tests and a property, the following
function returns either
Nothing when tests pass or
Just a counterexample
encoded as an
counterExample :: (Listable a, Express a) => Int -> (a -> Bool) -> Maybe Expr counterExample maxTests prop = listToMaybe [expr x | x <- take maxTests list, not (prop x)]
> counterExample 100 (\(x,y) -> x + y == y + x) Nothing > counterExample 100 (\x -> x == x + x) Just (1 :: Integer) > counterExample 100 (\xs -> nub xs == (xs :: [Int])) Just ([0,0] :: [Int])
Before moving on to generalize counterexamples, we need a way to compute ground
expressions from an expression with variables. For that, we will use
grounds :: Expr -> [Expr] grounds e = map (e //-) . concat $ products [mapT ((,) v) (tiersFor v) | v <- nubVars e] tiersFor :: Expr -> [[Expr]] tiersFor e = case show (typ e) of "Int" -> mapT val (tiers `asTypeOf` [[undefined :: Int]]) "Bool" -> mapT val (tiers `asTypeOf` [[undefined :: Bool]]) "[Int]" -> mapT val (tiers `asTypeOf` [[undefined :: [Int]]]) "[Bool]" -> mapT val (tiers `asTypeOf` [[undefined :: [Bool]]]) _ -> 
Above, we restrict ourselves to
[Bool] as test
types. So we can now compute the grounds of an expression with variables:
> grounds (value "not" not :$ var "p" (undefined :: Bool)) [ not False :: Bool , not True :: Bool ] > grounds (value "&&" (&&) :$ var "p" (undefined :: Bool) :$ var "q" (undefined :: Bool)) [ False && False :: Bool , False && True :: Bool , True && False :: Bool , True && True :: Bool ]
To compute candidate generalizations from a given counter-example, we use the following function:
candidateGeneralizations :: Expr -> [Expr] candidateGeneralizations = map canonicalize . concatMap canonicalVariations . gen where gen e@(e1 :$ e2) = [holeAsTypeOf e | isListable e] ++ [g1 :$ g2 | g1 <- gen e1, g2 <- gen e2] ++ map (:$ e2) (gen e1) ++ map (e1 :$) (gen e2) gen e | isVar e =  | otherwise = [holeAsTypeOf e | isListable e] isListable = not . null . tiersFor
The need for
isListable above makes sure we only replace by variables what we
can enumerate. Our candidate generalizations are listed in non-increasing
order of generality:
> candidateGeneralizations (value "not" not :$ val False) [ p :: Bool , not p :: Bool ] Prelude> candidateGeneralizations (value "||" (||) :$ val False :$ val True) [ p :: Bool , p || q :: Bool , p || p :: Bool , p || True :: Bool , False || p :: Bool ]
For a given maximum number of tests, property and counter-example, the following function returns a counter-example generalization if one is found. It goes through the list of candidate generalizations and returns the first for which all tests fail.
counterExampleGeneralization :: Express a => Int -> (a -> Bool) -> Expr -> Maybe Expr counterExampleGeneralization maxTests prop e = listToMaybe [g | g <- candidateGeneralizations e , all (not . prop . evl) (take maxTests $ grounds g)]
We can finally define our
check function, that will test a property and
report a counterexample and a generalization when either are found.
check :: (Listable a, Express a) => (a -> Bool) -> IO () check prop = putStrLn $ case counterExample 500 prop of Nothing -> "+++ Tests passed.\n" Just ce -> "*** Falsified, counterexample: " ++ show ce ++ case counterExampleGeneralization 500 prop ce of Nothing -> "" Just g -> "\n generalization: " ++ show g ++ "\n"
Now we can find counterexamples and their generalizations:
> check $ \xs -> sort (sort xs :: [Int]) == sort xs +++ Tests passed. > check $ \xs -> length (nub xs :: [Int]) == length xs *** Falsified, counterexample: [0,0] :: [Int] generalization: x:x:xs :: [Int] > check $ \x -> x == x + (1 :: Int) *** Falsified, counterexample: 0 :: Int generalization: x :: Int > check $ \(x,y) -> x /= (y :: Int) *** Falsified, counterexample: (0,0) :: (Int,Int) generalization: (x,x) :: (Int,Int)
u-Extrapolate has some limitations:
- it only supports properties with one argument (uncurried);
- it only supports generalization of
- there is no way to configure the number of test arguments.
Please see Extrapolate for a full-featured version without the above limitations and with support for conditional generalizations.
Example 4: u-Speculate
Using Express, it takes less than 70 lines of code to define a function
speculateAbout that conjectures equations about a set of functions based on
the results of testing:
> speculateAbout [hole (undefined :: Bool), val False, val True, value "not" not] [ not False == True :: Bool , not True == False :: Bool , not (not p) == p :: Bool ] > speculateAbout > [ hole (undefined :: Int) > , hole (undefined :: [Int]) > , val ( :: [Int]) > , value ":" ((:) :: Int -> [Int] -> [Int]) > , value "++" ((++) :: [Int] -> [Int] -> [Int]) > , value "sort" (sort :: [Int] -> [Int]) > ] [ sort  ==  :: Bool , xs ++  == xs :: Bool ,  ++ xs == xs :: Bool , sort (sort xs) == sort xs :: Bool , sort [x] == [x] :: Bool , [x] ++ xs == x:xs :: Bool , sort (xs ++ ys) == sort (ys ++ xs) :: Bool , sort (x:sort xs) == sort (x:xs) :: Bool , sort (xs ++ sort ys) == sort (xs ++ ys) :: Bool , sort (sort xs ++ ys) == sort (xs ++ ys) :: Bool , (x:xs) ++ ys == x:(xs ++ ys) :: Bool , (xs ++ ys) ++ zs == xs ++ (ys ++ zs) :: Bool ]
u-Speculate has some limitations:
- it sometimes prints redundant equations;
- although it usually runs quickly with less than 6 symbols, runtime is exponential with the number of symbols given, providing it with more than a dozen symbols can make it run for several minutes or hours;
- there is no way to configure the size limit of reported equations;
- it only supports variables of
Please see Speculate for a full-featured version without the above limitations.
For a detailed documentation, please see Express’s Haddock documentation.