A simple, but complete, tutorial for how to use Logic.Ltl. This does not cover

• using higher-order effects in the LTL setting, and
• combining several different effects in one test scenario.

If you're reading the Haddock documentation, consider reading the source, it'll make more sense.

To use this library, you need a type class of monads that captures the behaviour you want to test. For the sake of this tutorial, let's take a key-value-store where the keys are Strings and the values are Integers.

We'll assume a number of traces written using this type class. These will most likely be manually written test cases that cover (some part of) the normal usage of the system you're testing.

Here, we'll only write two slightly silly examples. The more different scenarios you cover in these "seed" traces, the more interesting variations will be generated later on.

What we'll test is an implementation of MonadKeyValue. We'll implement it very simply, but note that the implementation of deleteValue is wrong: we never delete anything from the store. We'll "find" this mistake later on.

This library is based on a custom effect system. There are a few macros that will make using it more convenient. You'll at least need the following language extensions (more extensions might be needed in more complex scenarios than this tutorial):

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}

The first macro will write an effect type corresponding to MonadKeyValue for us, and give it the name MonadKeyValueEffect:

The type MonadKeyValueEffect is an abstract representation of the class MonadKeyValue. This means that for each method of the class, there's a constructor of the effect type:

• for storeValue :: String -> Integer -> m (), there is StoreValue :: String -> Integer -> MonadKeyValueEffect m (),
• for getValue :: String -> m Integer, there is GetValue :: String -> MonadKeyValueEffect m Integer, and
• for deleteValue :: String -> m (), there is DeleteValue :: String -> MonadKeyValueEffect m ().

We thus have a reification of computations in MonadKeyValue. This reification will be used to build ASTs, which can then be interpreted in flexible ways.

There's also a macro to define some instances that will make this convenient.

The testing method explained in this tutorial consists in deploying single-step modifications while interpreting an AST. The AST will be built from abstract representations of actions (i.e. the constructors of effect types like MonadKeyValueEffect), and we'll interpret it into some suitable monad (here, that'll be KeyValueT m).

So, we'll first have to define a type of single-step modifications, and explain how they should change the interpretation of actions. The single-step modifications have no meaning in and of them themselves, as they are only explained by how they apply to the constructors of MonadKeyValueEffect.

Our modification type KeyValueMod captures two behaviours:

• When noOverwrite is True, the intended meaning is that storeValue should be ignored when it replaces the value (i.e., when the key is already present in the store)
• renameKey will change the keys used by any action with a prescribed function.

The InterpretMod instance now makes these intended meanings explicit. The function interpretMod describes, for each constructor of MonadKeyValueEffect, how it should be interpreted under a modification:

• Whenever the there's a modification that might apply, we'll try to apply it using the AttemptModification constructor.
• When the modification applies, we signal that success by wrapping the return value of the action in a Just.
• When the modification doesn't apply, we return Nothing.
• Whenever there's no modification, we have nothing to apply, so we return SkipModification. This will mean that the operation will be performed as usual.
• A third possibility, which is not shown here, is returning PassModification instead of AttemptModification or SkipModification, which would mean to do the operation without modification as usual, but remember the modification for the next step. This can be thought of as making the operation invisible to modifications.

Here are two smart constructors for modifications, one for creating a modification that transforms keys solely, the other that only ignores overwrites:

The module Logic.Ltl implements one way to combine single-step modifications into composite modifications that apply to traces: a formula in an LTL-like language determines when to apply the single-step modifications.

The evaluation of such Ltl formulas sometimes makes it necessary to try applying two single-step modifications on the same step. The Semigroup instance describes how they should combine.

The module Logic.Ltl provides the wrapper type LtlAST mod ops. Here, ops is the list of effect types related to our domain. In our case, it will have to contain MonadKeyValueEffect and MonadErrorEffect KeyValueError. The Template Haskell macros we used above make it so that

LtlAST mod '[MonadKeyValueEffect, MonadErrorEffect KeyValueError]

is an instance of MonadKeyValue and MonadError KeyValueError. The parameter mod is the type of single-step modifications; here it is KeyValueMod.

In addition to all the MonadKeyValue and MonadError functions, the LtlAST also gives you access to the function

modifyLtl :: Ltl mod -> LtlAST mod ops a -> LtlAST mod ops a

This is what makes it possible to deploy composite Ltl modifications: wrap the part of the computation you want to modify in modifyLtl with the Ltl formula of your choice.

The module Logic.Ltl also provides

interpretLtlAST :: forall mod m ops a. (Semigroup mod, MonadPlus m, InterpretEffectsLtl mod m tags ops) => LtlAST mod ops a -> m a

which interprets the LtlAST mod ops into any suitable monad m. Here, "suitable" means:

• All of the effects in ops have one of the following three instances:

  • InterpretMod mod m (this is what we have here)
  • InterpretLtlHigherOrder mod m (this is for higher order effect types, we're not interested in that here)
  • InterpretEffectStateful (Const [Ltl mod]) m (this is a low-level class used to implement the LTL framework itself)
• m is a MonadPlus. This is necessary because there might be several ways to satisfy an Ltl formula. The whole point of using Ltl do describe modifications of a single trace is to try all of the possible ways to apply the formula. Sometimes, this requires defining a custom MonadPlus instance for the monad (or transformer) we're interested in.

Using interpretLtlAST, we can write a convenience function that will interpret an LtlAST of MonadKeyValueEffects and return the final return value and state of the store.

Note how we type-apply interpretLtlAST to a list of "tags" of kind LtlInstanceKind: These tags specify, in order, which of the three instances described above we expect the effects to have.

The InterpretEffectStateful instance for MonadErrorEffect is imported from Effect.Error.Passthrough, and is implemented in a generic way so as to ignore every modification: we only care about modifying MonadKeyValue actions.

By far the most commonly used Ltl formula is somewhere.

In our first example, we try applying the modification noStoreOverride to some action in the swapTrace. There are two actions where the modification applies, namely the third and fourth storeValues:

swapTrace = do
  storeValue "a" 1
  storeValue "b" 2
  a <- getValue "a"
  b <- getValue "b"
  storeValue "a" b   -- replaced by no-op in branch 1
  storeValue "b" a   -- replaced by no-op in branch 2
  a' <- getValue "a"
  b' <- getValue "b"

So, we expect to have two modified traces, where both "a" and "b" share the same value, and that's indeed the case:

>>> exampleSomewhereSwap
[(Right (1,1),fromList [("a",1),("b",1)]),
 (Right (2,2),fromList [("a",2),("b",2)])]

In the deleteTrace, we expect noStoreOverride never to apply as there should be no override. However, it applies because our implementation of deleteKey does not actually delete anything.

deleteTrace = do
  storeValue "a" 1
  storeValue "b" 2
  deleteValue "a"
  storeValue "a" 2 -- replaced by no-op
  getValue "a"

We have "discovered" the bug!

>>> exampleSomewhereDelete
[(Right 1,fromList [("a",1),("b",2)])]

Another very commonly used Ltl formula is everywhere. It must apply the given single-step modification to every action in the AST. If it is not applicable somewhere, then there will be no output trace.

So, when we apply everywhere noStoreOverride to the swapTrace, we'll get no results, because not all storeValues in that trace replace the value at a key.

>>> exampleEverywhereSwap
[]

On the other hand, renameKeys always applies, and hence we can successfully apply it to, say the deleteTrace, and thus prove that its behaviour is independent under renaming of keys.

>>> exampleEverywhereDelete
[(Right 2,fromList [("anew",2),("bnew",2)])]

Note that, unlike somewhere, everywhere doesn't imply that any modification is applied. Applying everywhere to an empty trace is successful, and returns one result:

>>> exampleEverywhereEmpty
[((),fromList [])]

In addition to somewhere and everywhere, it is also possible to require the application of a modification starting from a specific position in a trace using there

>>> exampleThere
[(Right (),fromList [("a",1),("b",2),("cnew",3),("d",4)]),
 (Right (),fromList [("a",1),("b",2),("c",3),("dnew",4)])]

Another idiom to accomplish the same without using there is to only apply modifyLtl after the first few actions:

>>> exampleNotThere
[(Right (),fromList [("a",1),("b",2),("cnew",3),("d",4)]),
 (Right (),fromList [("a",1),("b",2),("c",3),("dnew",4)])]

Finally, it is possible to create formulas by hand using the Ltl constructors. In this example, we add "new" to the key of the two first instructions of @deleteTrace

>>> exampleCustom
[(Right (),fromList [("anew",1),("bnew",2),("c",3),("d",4)])]