verifiable-expressions-0.6.0: An intermediate language for Hoare logic style verification.

Safe HaskellNone
LanguageHaskell2010

Language.Expression.Example

Contents

Description

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.

Synopsis

Operators

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.

data SimpleOp t a where Source #

An operator type has two arguments. t is a type constructor used to refer to expressions. a is the semantic type of the expression formed by the operator.

Constructors

Add :: t Integer -> t Integer -> SimpleOp t Integer

Given two int expressions, we may add them. Notice how we refer to expressions recursively with the type constructor parameter t.

Equal :: t Integer -> t Integer -> SimpleOp t Bool

Given two int expressions, we may compare them for equality. Notice the types of the arguments to the operator do not appear in the result type at all.

IfThenElse :: t Bool -> t Integer -> t Integer -> SimpleOp t Integer

Operator constructors can have any number of arguments, and you can mix argument types.

Literal :: Integer -> SimpleOp t Integer

An operator does not have to actually combine expressions. It may produce an expression from a basic value, i.e. a literal int. HFree itself does not provide literals so they must be encoded in operators.

Instances
HTraversable SimpleOp Source # 
Instance details

Defined in Language.Expression.Example

Methods

htraverse :: Applicative f => (forall (b :: u). t b -> f (t' b)) -> SimpleOp t a -> f (SimpleOp t' a) Source #

hsequence :: Applicative f => SimpleOp (Compose f t) a -> f (SimpleOp t a) Source #

HFunctor SimpleOp Source # 
Instance details

Defined in Language.Expression.Example

Methods

hmap :: (forall (b :: u). t b -> t' b) -> SimpleOp t a -> SimpleOp t' a Source #

HFoldableAt Identity SimpleOp Source # 
Instance details

Defined in Language.Expression.Example

Methods

hfoldMap :: (forall (b :: k). t b -> Identity b) -> SimpleOp t a -> Identity a Source #

HFoldableAt SBV SimpleOp Source # 
Instance details

Defined in Language.Expression.Example

Methods

hfoldMap :: (forall (b :: k). t b -> SBV b) -> SimpleOp t a -> SBV a Source #

Type Classes

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.

Variables

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.

data SimpleVar a where Source #

Notice that a is a phantom type here (and it will be for most variable type constructors). It is only used to restrict the type of values that are representable by these variables. In this case, we only want to be able to store integers so the only constructor has return type Integer. It also contains a String to be used as the variable name.

Constructors

SimpleVar :: String -> SimpleVar Integer 

Expressions

type SimpleExpr = HFree SimpleOp SimpleVar Source #

Now that we have defined our operators and variables, HFree SimpleOp SimpleVar a is a syntax tree for a strongly typed expresson language.

A DSL

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

Example Expression

exampleExpr :: SimpleExpr Integer Source #

Here's an example of expression written using this DSL.

exampleExpr = ifThenElse (var "x" .== lit 10) (var "y") (var "y" .+ lit 5)
exampleExpr ~ if (x = 10) then y else y + 5

Expression Manipulation

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

Substitution

^>>= substitutes variables inside expressions.

exampleExpr2 :: SimpleExpr Integer Source #

exampleExpr, with x replaced by z + 5.

exampleExpr2 =
  exampleExpr ^>>= v@(SimpleVar nm) ->
  if nm == "x" then var "x" ^+ lit 5 else hpure v

exampleExpr2 ~ if ((z + 5) = 10) then y else y + 5

Traversal

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

evalXOrY :: SimpleVar a -> Maybe (Identity a) Source #

This is a function that knows the value of variables with certain names. It will return Nothing if it doesn't know how to evaluate a particular variable.

evalXOrY (SimpleVar "x") = Just 1
evalXOrY (SimpleVar "y") = Just 2
evalXOrY _ = Nothing

It might seem strange that we can return Just (Identity 1) when the function says it returns a Maybe (Identity a) for polymorphic a. This works because the constructor SimpleVar must be Integer-valued, so when we match on it, GHC generates the constraint a ~ Integer and it will happily accept an Integer.

Notice that, for s ~ SimpleVar, t ~ Identity and f ~ Maybe,

evalXOrY :: forall a. s a -> f (t a)

This means that we can traverse using this function:

>>> htraverse evalXOrY exampleExpr
htraverse evalXOrY exampleExpr :: Maybe (HFree SimpleOp Identity Integer)
htraverse evalXOrY exampleExpr ~ Just (if (1 = 10) then 2 else 2 + 5)
>>> htraverse evalXOrY exampleExpr2
htraverse evalXOrY exampleExpr2 :: Maybe (HFree SimpleOp Identity Integer)
htraverse evalXOrY exampleExpr2 ~ Nothing

There was a variable (z) that evalXOrY didn't know how to evaluate, so the traversal resulted in Nothing!

Evaluating Expressions

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

Evaluating Variables Symbolically

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

evalVarSymbolic :: SimpleVar a -> StateT (Map String (SBV Integer)) Symbolic (SBV a) Source #

Here's a function that converts variables in SimpleVar to symbolic values. It needs a Map String (SBV Integer) stateful environment in order to remember variables that already have symbolic values, because SBV will give you different variables on two different calls of symbolic x for the same x.

Evaluating Expressions Symbolically

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

evalSimpleExprSymbolic :: SimpleExpr a -> StateT (Map String (SBV Integer)) Symbolic (SBV a) Source #

Now we can evaluate expressions symbolically and use sbv to prove things about them.

evalSimpleExprSymbolic = hfoldTraverse evalVarSymbolic

examplePredicate :: Predicate Source #

Let's ask sbv to prove that our expression always returns a value no less than the variable y.

examplePredicate = flip evalStateT mempty $ do
  expr <- evalSimpleExprSymbolic exampleExpr
  y <- evalSimpleExprSymbolic (var "y")
  return (expr .>= y)
>>> isTheorem examplePredicate
True