Language.Expression provides a way of forming strongly types expression languages from operators, via HFree. This module is an explanation of how that works, via a simple example.

This module is intended to be read via Haddock.

An operator is a type constructor op of kind (* -> *) -> * -> *. op t a should be seen as a way of combining t-objects which has a result type a.

SimpleOp is an example of an operator type.

Most useful operators are instances of HFunctor (which provides hmap) and HTraversable (which provides htraverse). These are higher-ranked analogues of Functor and Traversable from base. Compare the type signatures of fmap and hmap:

fmap :: (Functor f) => (a -> b) -> f a -> f b
hmap :: (HFunctor h) => (forall b. s b -> t b) -> h s a -> h t a

fmap transforms the *-kinded type argument to f, while hmap transforms the (* -> *)-kinded type constructor argument to h.

So in order for an operator to have an instance of HFunctor, it must be possible to swap out sub-expressions inside it. This is the case for our SimpleOp.

HTraversable has a similar relationship with Traversable. htraverse adds an applicative context to 'hmap'\'s transformations:

traverse :: (Traversable t, Applicative f) => (a -> f b) -> t a -> f (t b)
htraverse :: (HTraversable h, Applicative f) => (forall b. s b -> f (t b)) -> h s a -> f (h t a)

There is a default implementation of hmap in terms of htraverse.

As well as operators, expressions contain variables. Variables are also strongly typed. A variable type v has kind * -> *. The type parameter tells us the type of the value that the variable is meant to represent.

We can write simple wrapper functions to form a DSL for our expression language.

If op is an HFunctor, then HFree op is an HMonad. HMonad defines hpure (c.f. pure or return):

hpure :: (HMonad h) => t a -> h t a
return :: (Monad m) => a -> m a

and ^>>= (c.f. >>=):

(>>=) :: (Monad m) => m a -> (a -> m b) -> m b
(^>>=) :: (HMonad h) => h s a -> (forall b. s b -> h t b) -> h t a

In the case of HFree op, hpure produces an expression containing a single variable:

hpure :: v a -> HFree op v a

^>>= substitutes variables inside expressions.

When op is an HTraversable, HFree is also an HTraversable. This can be used, for example, to evaluate variables in an expression.

The HFoldableAt type class provides the mechanism for evaluating operators, and hence expressions.

hfoldMap :: (HFoldableAt k h) => (forall b. t b -> k b) -> h t b -> k b

Implemented in terms of this is

hfoldTraverse
  :: (HFoldableAt k h, HTraversable h, Applicative f)
  => (forall b. t b -> f (k b))
  -> h t a
  -> f (k a)
hfoldTraverse f = fmap (hfoldMap id) . htraverse f

This function will allow us to evaluate our expressions to ground values:

>>> hfoldTraverse evalXOrY exampleExpr
Just (Identity 7)

>>> hfoldTraverse evalXOrY exampleExpr2
Nothing

With the help of sbv, we can evaluate expressions symbolically in order to prove things about them.

We need an instance of HFoldableAt SBV SimpleOp to do symbolic evaluation, implemented like so:

instance HFoldableAt SBV SimpleOp where
  hfoldMap = implHfoldMap $ s -> case s of
    Add x y          -> x + y
    Equal x y        -> x .== y
    IfThenElse x y z -> ite x y z
    Literal x        -> literal x