Function Optimization

Equational reasoning is not only useful to verify existing code, it can also be used to derive new, more performant function definitions from specifications.

Example: Reversing a List

The reverse function that we defined in before was simple and easy to reason about, but it is rather inefficient. In particular, for each element in the input list, reverse appends it to the end of the reversed tail of the list:

  reverse (x:xs) = reverse xs ++ [x]

Because the runtime of ++ is linear in the length of its first argument, the runtime of reverse is quadratic. For example, reversing a list of ten thousand elements would take around fifty million reduction steps, which is excessive.

To improve the performance, we would like to define a function that does the reversing and appending at the same time; that is, to define a new function

We now seek to derive an implementation for reverseApp that satisfies this specification and is efficient.

Step 0: Specification We begin by writing a definition for reverseApp that trivially satisfies the specification and is hence accepted by Liquid Haskell, but is not yet efficient:

We then seek to improve the definition for reverseApp in step-by-step manner, using Liquid Haskell's equational reasoning facilities to make sure that we don't make any mistakes, i.e., that we do not violate the specification.

Step 1: Case Splitting Most likely, the function has to analyse its argument, so let us pattern match on the first argument xs and update the right-hand side accordingly:

Liquid Haskell ensures that our pattern match is total, and that we updated the right-hand side correctly.

Step 2: Equational Rewriting Now we want to rewrite the right-hand sides of reverseApp to more efficient forms, while ensuring that our function remains correct. To do so, we can use the (==.) operator to show that each change we make gives us the same function. Whenever we add a line, Liquid Haskell confirms that this step is valid. We begin by simply expanding definitions:

We're still using reverse, so we're not quite done. To finish the definition, we just need to observe that the last line has the form reverse as ++ bs for some lists as and bs. This is precisely the form of the specification for reverseApp as bs, so we can rewrite the last line in terms of reverseApp:

In summary, our definition for reverseApp no longer mentions the reverse function or the append operator. Instead, it contains a recursive call to reverseApp, which means we have derived the following, self-contained definition:

reverseApp :: [a] -> [a] -> [a]
reverseApp []     ys = ys
reverseApp (x:xs) ys = reverseApp xs (x:ys)

The runtime performance of this definition is linear in the length of its first argument, a significant improvement.

Step 4: Optimizing reverse The goal of this exercise was of course not to have an efficient reverse-and-append function, but to have an efficient reverse function.
However, we can define this using reverseApp, again starting from its specification and deriving the code that we want to run. Here we need to turn reverse xs into reverse xs ++ ys for some list ys. This requires us to use the theorem rightIdP:

The above derivation follows the same steps as the pen-and-paper version in Graham's book, with one key difference: the correctness of each step, and the derived program, is now automatically checked by Liquid Haskell.

Example: Flattening a Tree

We can use the same technique to derive an optimized function for flattening trees. Our trees are binary trees with integers in the leaves, as in Graham's book:

We wish to define an efficient function that flattens such a tree to a list. As with reverse, we begin with a simple but inefficient version that uses the append operator:

Because we want to refer to this function in our specifications and reasoning, we instruct Liquid Haskell to lift it to the refinement type level using reflect keyword. Liquid Haskell’s structural termination checker accepts this and all following functions on trees, and there is no need to define a measure on trees.

We can use flatten as the basis of a specification for a more efficient version. As before, the trick is to combine flatten with list appending and define a function

with the specification flattenApp t ns == flatten t ++ ns, which we can state as a Liquid Haskell type signature:

As in the previous example, we begin by using the specification as a correct but inefficient implementation

and use equational reasoning in Liquid Haskell to work our way towards an implementation that avoids the use of the inefficient flatten and append functions:

Again, this derivation serves both as an implementation and a verification, and is operationally equivalent to:

flattenApp :: Tree -> [Int] -> [Int]
flattenApp (Leaf n)   ns = n:ns
flattenApp (Node l r) ns =
  flattenApp l (flattenApp r ns)

Finally, we can then derive the optimized flatten function by means of the following simple reasoning:

In conclusion, the derivation once again follows the same steps as the original pen-and-paper version, but is now mechanically checked for correctness.

Appendix

Since the online demo does not let us import functions, we close by repeating the required function definitions and theorems on lists.