Dynamically-typed expressions involving applications and variables.
|Version on this page:||0.1.2|
|LTS Haskell 20.24:||1.0.10|
|Stackage Nightly 2023-06-04:||1.0.10|
|Latest on Hackage:||1.0.10|
Module documentation for 0.1.2
Express is a library for manipulating dynamically typed Haskell expressions.
Data.Dynamic but with support for encoding applications and
It provides the
Expr type and over a hundred functions for
building, evaluating, comparing, folding, canonicalizing and matching
Exprs. See Express’s Haddock documentation for more details.
This library has been used successfully in the implementation of Speculate and Extrapolate.
To install the latest Express version from Hackage, just run:
$ cabal update $ cabal install express
For types that are
we can use
val to encode values as
> 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
As seen above, the
Show instance for
Expr produces a string with the
encoded value and it’s type.
For types that aren’t
Show instances, like functions,
we can use [
value] to encode values as
> let notE = value "not" not > :t notE notE :: Expr > print notE not :: Bool -> Bool
:$ we can apply function valued
Exprs, to other Exprs.
> let notFalse = notE :$ false > :t notFalse notFalse :: Expr > notFalse not False :: Bool
evaluate and [
eval] we can evaluate
Exprs back into a regular Haskell value.
> 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 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 ]
Please see the u-Speculate example in the eg folder for the full code
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.
For more examples, see the eg and bench folders.