A tutorial for how to use Logic.Ltl with higher-order effects. The explanations here assume you've understood the simple tutorial in Examples.Ltl.Simple.

Our domain will be a low level, Turing-complete, abstract machine called MonadMiniLang which is based on a stack of integers and booleans and can raise three different errors. Values can be popped and pushed, arbitrary text can be printed, and two control structures are present: if_ and while_.

These two latter operations are what makes MonadMiniLang a higher order domain: There are nesting operations, that is, operations that have sequences of operations in the same monad as parameters.

In Graft, nested operations must occur in positive position for conceptual and technical reasons. As a reminder, x is in positive position in t if it stands before an even number of ->s, otherwise it is in negative position. A few examples:

• In a -> b, a is in negative position, b in positive
• position.
• In (a -> b) -> c, a and c are in positive position, and b is in negative position.
• In Maybe ((a -> [b]) -> c) -> d, d and b are in positive position, and a and c are in negative position.

A concrete implementation for our domain: we use

• a list of values as inner state to account for the stack
• a writer to allow printing strings using echo
• an exception to cover possible errors

As in the simple tutorial, the MonadPlus instance is necessary boilerplate for the interpretation of Ltl formulas, since there might be several ways to satisfy one formula, and we want to try them all.

To obtain the effects associated with MiniLang for free, we call the same macros as in Examples.Ltl.Simple which also work in higher order settings.

Our type of modifications is a conjunction of a function to be applied before pushing a value, and a function to be applied after poping a value. To combine those within a Semigroup instance, we compose them while accounting for the fact that they can return Nothing.

Again, as explained in the simple tutorial, the Semigroup instance is necessary because evaluation of Ltl formulas might sometimes make it necessary to apply more than one modification on the same operation.

Meaning is given to the single step modifications through their interpretation over our domain. This is what the class InterpretLtlHigherOrder is for. There are two main differences with the first order case:

• The interpretation function directly handles Ltl formulas. (Remember that the InterpretMod instance in the simple tutorial only has to handle single-step modifications.) This is because the approach based on applying atomic modifications to single operations breaks down for higher-order operations: a single higher-order operation may contain sequences (ASTs) of operations.
• An explicit distinction needs to be made between first-order and higher-order effect constructors, by using Direct and Nested respectively.

Considering the second difference:

• Using Direct signals that the operation at hand is first order, and you can proceed as if writing an InterpretMod instance, as explained in the simple tutorial.
• Using Nested means the operation is of higher order. This case is detailed below.

Handling higher order operations:

In the first order setting, we have the convenient class InterpretMod which allows us to specify how single-step modifications should be applied on operations. In the higher order setting the question is different: applying a single step modification on a nested operation makes no sense because it will likely contain several such operations, thus we provide the whole set of formulas to be applied currently and leave it to the user as to how they should be handling those. While it seems complicated, it is actually pretty straighforward in most cases as the user has sufficient domain knowledge to know how and when the nested blocks will be executed.

In the example:

Let's explain if_ here. The typical behaviour of if_ will be to evaluate the condition and pass the formula that modifies the remainder of the computation to either of the two branches, depending on whether the condition was true or false. In the case of our example, evaluation the condition is itself an operation, namely a pop. So, we will first consume the next single step modification and apply it to that pop. If that was successful, we'll pass on the remaining formulas to the correct block depending on the result of the (possibly modified) result of evaluating the condition.

Note how we use the function nowLaterList which, from a list of Ltl formulas, creates a list of pairs of a modification to be applied now and the remaining formulas. This function will likely often be called in higher order operations.

As in the simple tutorial, we can use the function interpretLtlAST to obtain a function that will interpret an LtlAST of MonadMiniLangEffect and MonadErrorEffect.

Note that the LtlInstanceKind for the MonadMiniLangEffect is InterpretLtlHigherOrderTag, since that's the instance that we implemented above: InterpretLtlHigherOrder MiniLangMod m MonadMiniLangEffect.

Again, the InterpretEffectStateful instance for MonadErrorEffect MiniLangError is the "passthrough" instance imported from Effect.Error.Passthtrough, which ignores all modifications: We're only interested in modifying MonadMiniLang operations in the program, not its generic error handling.

As in the simple simple tutorial, we can apply the modifyLtl function to modify the MonadMiniLang operations in the program.

>>> exampleSomewhere
[((Right -42,"Pushing 42"),[]),
 ((Right -42,"Pushing 42"),[])]

Let's look at a more interesting example with a higher-order operation, if_.

>>> exampleIf flipIntegers True
[((Right (),""),[MiniLangInteger (-42)]]

>>> exampleIf flipIntegers False
[]

The two runs above show that we only modify the "else" branch of the if_ when it is executed: in the second run, no modification is applied, because no push or pop involving an integer happens.

The next two runs are more involved, because we modify booleans, which are intrinsically very relevant for if_s. Let's mark the places that are potentially modified:

do
  pushBoolean intOrBool    -- (1) because we push a boolean
  if_                      -- (2) because 'if_' pushes a boolean
    (pushInteger 42)
    (pushBoolean True)     -- (3) because we push a boolean

The modality somewhere requires that we either modify the pushBoolean at (1), or modify some later push or pop of a boolean. If intOrBool is initially True, that means we have two options:

• modify at (1), which means that the we'll pop a False at (2). In this scenario, we'll execute the 'else' branch, which will push a True at (3).
• modify at (2), which also means that we'll pop a False at (2). We'll consequently also execute the execute the 'else' branch, which will push a True at (3).

Note that we'll never apply a modification at (3), because in both cases, the requirements of somewhere are already satisfied.

>>> exampleIf flipBools True
[((Right (), ""), [MiniLangBoolean True]),
 ((Right (), ""), [MiniLangBoolean True])]

For our last run, let's look at the case where intOrBool is False. In that case, the following three scenarios are possible:

• modify at (1), which means that we'll pop a True at (2). So, we'll execute the 'then' branch, which will push a '42'.
• modify at (2), which means that we'll pop a True at (2). So, we'll execute the 'then' branch, which will push a '42'.
• If we don't modify at (1) or (2), we'll execute the 'else' branch, which will push a False (modified from True) at (3).

>>> exampleIf flipBools False
[((Right (),""),[MiniLangInteger 42]),
 ((Right (),""),[MiniLangInteger 42]),
 ((Right (),""),[MiniLangBoolean False])]

Finally, for a more testing-flavoured example, we can check the property that the programs only interact with the stack through the push and pop operations, by applying everywhere flipBoth. Effectively, this modification means that the entries on the stack will always be the inverse of their "actual" values, and that the meaning of push and pop also contains reversing this polarity.

>>> exampleFlipFibonacci
True