About  Posts  Feed

Static analysis using functional abstraction

Published

A look at some functional abstractions that enable static analysis.

This is a common problem: you want to write a program that can explain itself without running it with real data:

In other words, we can perform runtime static analysis on the code. Runtime static analysis means that we must run the program to analyze it, but we don’t have to provide any user inputs to it.

Some programming languages can use reflection to accomplish some of this, and it’s a bit similar in the sense that you are not running the program with user inputs. But it’s also very different from what I’m talking about here because with reflection you need to create a special program to analyse the code. It also requires support from the runtime which many languages simply don’t have.

The problem

Let’s first zoom into the issue to understand what the problem is. If we take a normal imperative program like the following:

foo :: Effect Number
foo = do
  x <- baz
  bar x

which is the same as this:

foo = baz `bind` \x -> bar x

we can observe that in order to evaluate bar we need the value x from baz. If we want to analyze this program without running it we are out of luck. In order to feed an x to bar x we must run baz.

We can also just look at the type signature of bind for Monad:

bind :: m a -> (a -> m b) -> m b
                     ^^^

and observe that in the second argument the term m b is inside a lambda, and these terms of type m b are the ones that we want to analyze and see statically without running the program. To make program analysis possible we must use other abstractions which don’t have the terms inside a lambda.

Applicative functors

One such abstraction is captured by the Apply/Applicative type class in Haskell/PureScript:

class Functor f => Apply f where
  apply :: f (a -> b) -> f a -> f b

In neither of the arguments f is inside a lambda, which is what we need in order to make static analysis on f possible. The f in the first argument is parameterized by a pure function a -> b which we don’t need to apply in order to know what the f is.

There are several ways we can design our Applicative data type so that it supports static analysis. The paper Free Applicative Functors (PDF) explains one approach using a “Free structure”. The Haskell package optparse-applicative uses a similar encoding to implement an argument parser that can generate a --help page from the program definition. The PureScript package argparse-basic on the other hand builds both the help and the parser in one go. Both libraries provide a similar API relying on Applicative.

Selective applicative functors

Selective Applicative Functors (PDF) are interesting.

class Applicative f <= Selective f where
  select :: forall a b. f (Either a b) -> f (a -> b) -> f b

First of all we can see that no term f x is inside a lambda, so that’s good in terms of static analysis. The point of Selective is that the second effect, f (a -> b), is optional. We can’t apply the callback a -> b if the first effect doesn’t provide an a. When the first effect returns a b, we can skip the second effect and just return the b.

We can see that Selective provides a static structure much like Applicative but it also allows for rudimentary branching logic – all the branches are “visible” statically. The branchS combinator is a good example of this:

branchS :: forall f a. Selective f => f Boolean -> f a -> f a -> f a
branchS i t e = select (map (bool (Left unit) (Right unit)) i) (map const t) (map const e)
  where
  bool x y test = if test then x else y

There are two possible branches that the computation might take. The one that is taken depends on the Boolean we get from the first effect. Since we can enumerate all the values of a Boolean, we can statically also enumerate all the possible consequences because neither of the branches are under a lambda term.

In the paper they explain how Selective Applicative Functors can be used in build systems to calculate dependencies statically without running the build.

Lifting to Category

There’s one other way to make static analysis possible even in the presense of dependencies between terms. Basically, you can take the callback from bind:

bind :: m a -> (a -> m b) -> m b
               ^^^^^^^^^^

and lift it to a data type:

data Star m a b = Star (a -> m b)
                       ^^^^^^^^^^

This eliminates the lambda term from the type you are composing. Instead of composing terms of m a you are now composing terms of the shape a -> m b. Essentially here we are composing “boxes” of inputs and outputs, without the possibility of knowing what the inputs and outputs are exactly. This forces you to work with more high level APIs like Category and Profunctor.

The most basic example is the compose function in the Category type class:

compose :: Category cat => cat b c -> cat a b -> cat a c

a2c :: Category cat => cat a c
a2c = compose b2c a2b

We can statically analyze the expression a2c and say that both a2b and b2c are used to compute the result. The same cannot be said if we write the composition “by hand” using plain function composition:

compose :: (b -> c) -> (a -> b) -> (a -> c)

a2c :: a -> c
a2c = compose b2c a2b

The reason, once again, is that the terms we are composing include lambda terms, and we can’t look inside them without applying them to some value.

Now, it might not be useful to analyze the program at this higher Category level but it could be useful in situtations where applicative composition is not possible. You could say that with this approach we can see what boxes are being composed, but we can’t see what those boxes contain. But remember, boxes can be composed of other boxes! There are combinators at your disposal from Category and the Profunctor hierarchy which provide ways to do this.

The tradeoff with this kind API is that it is much more high-level and those combinators can be quite difficult to work with, at least it takes some time getting used to. Because it’s so high-level, the analysis you can do on the terms is limited to be on a higher level as well.

Conclusion

I’ve shown a few ways we can approach runtime static analysis using functional abstraction. We’ve seen how Monad is doesn’t have the necessary properties while Applicative Functors do. There is also Selective Applicative Functors that sit between Applicative and Monad, which do have similar qualities for doing limited runtime static analysis. Sometimes we can even reach for a higher level abstraction with Category and Profunctor to be able to analyze programs on a higher level. I didn’t even mention Monoids or Semirings which have good properties for static analysis since they are even simpler than the ones mentioned in this post. That will have to be another post!