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:
- A CLI argument parser that can generate the
--helpoutput without providing it with any actual inputs
- A build system that can show you the dependencies between build steps without running the actual build
- A formula that can visualize itself without providing it with any 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.
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
If we want to analyze this program without running it we are out of luck.
In order to feed an
bar x we must run
We can also just look at the type signature of
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.
One such abstraction is captured by the
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 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
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
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
When the first effect returns a
b, we can skip the second effect and just return the
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.
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 :: 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
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
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.
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
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!