A Computational Lambda Calculus for Applicative Functors

These days, most people are familiar with using monads to structure functional programs, and are also familiar with Haskell's do-notation for writing monadic code. Slightly less well-known is the fact that the do-notation actually originates in Moggi's original 1991 paper on monads, in which he gave the following type-theoretic introduction and elimination rules for monadic types: $$ \newcommand{\val}[1]{\mathsf{val}\,{#1}} \begin{array}{ll} \rule{\judge{\Gamma}{e}{A}} {\judge{\Gamma}{\val{e}}{T(A)}} & \rule{\judge{\Gamma}{e}{T(A)} \qquad \judge{\Gamma, x:A}{e'}{T(C)}} {\judge{\Gamma}{\letv{\val{x}}{e}{e'}}{T(C)}} \end{array} $$

In the last few years, Ross Patterson and Conor McBride have begun advocating using what they call applicative functors to structure programs, which are strong lax monoidal endofunctors. Applicatives are less general than monads, and consequently support a stronger equational theory. (See also the discussion by Edward Z. Yang and Tomas Petricek, which prompted me to write this note.)

Suppose that $C$ is our semantic category, and that it comes equipped with products $A \times B$. Then a lax monoidal endofunctor $(F, \phi, i)$ is an endofunctor $F : C \to C$, together with a pair of natural transformations $\phi_{A,B} : F(A) \times F(B) \to F(A \times B)$ and $i : 1 \to F(1)$.

These maps satisfy some coherence conditions, which basically ensure that it doesn't matter if you re-associate a product before or after applying the monoidal functor. Below, I give the interesting one, for the product. (This is also an experiment to use SVG in my blog, so let me know if it blows up for you.)

The basic way to read this diagram is that it's telling you that it doesn't matter how you do the computations to collect the values. You can either use $\phi_{A,B}$ followed by $\phi_{A \times B, C}$, or you can use use $\phi_{B, C}$ followed by $\phi_{A, B \times C}$, but either way you get the same computation.

For a functor to be strong, we also need a strength $\sigma_{A,B} : F(A) \times B \to F(A \times B)$. This is the usual presentation of this condition, since it makes the semantics easier to do. However, for purposes of intution, it's a little bit mysterious.

Strength gets less mysterious when presented as the (equivalent) condition that you have a family of maps $\mathrm{fmap} : (A \Rightarrow B) \to (F(A) \Rightarrow F(B))$. This means that in programming language terms, having a strength is equivalent to saying that the functor $F$ has a map operation definable in the language.

With these preliminaries aside, we can see the type theory for applicative functors below: $$ \begin{array}{ll} \rule{\judge{\cdot; \Delta, \Gamma}{e}{A}} {\judge{\Delta; \Gamma}{\val{e}}{F(A)}} & \rule{\judge{\Delta; \Gamma}{e}{F(A)} \qquad \judge{\Delta, u:A; \Gamma}{e'}{C}} {\judge{\Delta;\Gamma}{\letv{\val{u}}{e}{e'}}{C}} \\ \rule{\judge{\Delta; \Gamma, x:A}{e}{B}} {\judge{\Delta; \Gamma}{\fun{x}{e}}{A \to B}} & \rule{\judge{\Delta; \Gamma}{e}{A \to B} \qquad \judge{\Delta; \Gamma}{e'}{A}} {\judge{\Delta; \Gamma}{e\;e'}{B}} \\ \rule{x:A \in \Gamma} {\judge{\Delta; \Gamma}{x}{A}} & \rule{\judge{\Delta;\Gamma}{e}{A} \qquad \judge{\Delta; \Gamma, x:A}{e'}{C}} {\judge{\Delta; \Gamma}{\letv{x}{e}{e'}}{C}} \end{array} $$

As you can see, the main difference is that we introduce a new context $\Delta$ of applicative variables. Applicative terms have a let-style eliminator, which binds the result of an applicative computation to a variable in the applicative context $\Delta$. However, the ordinary variable rule cannot look at variables from $\Delta$ -- it can only look at variables from $\Gamma$. We only gain access to $\Delta$ when we introduce a term $\val{e}$ of type $F(A)$, when in the premise we move all the variables in $\Delta$ into the ordinary variable zone.

The beta- and eta-rules for this calculus are pretty much what you'd expect: $$ \begin{array}{lcl} \letv{\val{x}}{\val{e}}{e'} & =_\beta & [e/x]e' \\ \letv{\val{x}}{e}{\val{x}} & =_\eta & e \\ \end{array} $$

I'm not totally sure what the commuting conversions are. I think the easiest thing would be to prove a normalization theorem to work those out. I might do that in a future post.

Now, we can also give a denotational interpretation. For readability, we suppress the maps re-associating and permuting variables, as well as anything to do with units. Semicolon is diagrammatic composition, as usual. $$ \begin{array}{l} \interp{\judge{\Delta;\Gamma}{x}{A}} = \\ \qquad \pi_2; \pi_x \\ \interp{\judge{\Delta;\Gamma}{\letv{x}{e}{e'}}{C}} = \\ \qquad \left\langle F(\Delta) \times \Gamma; \interp{\judge{\Delta;\Gamma}{e}{A}}\right\rangle ; \interp{\judge{\Delta; \Gamma, x:A}{e'}{C}} \\[1em] \interp{\judge{\Delta; \Gamma}{\fun{x}{e}}{A \to B}} = \\ \qquad \lambda(\interp{\judge{\Delta;\Gamma,x:A}{e}{B'}}) \\ \interp{\judge{\Delta; \Gamma}{e\;e'}{B}} = \\ \qquad \left\langle \interp{\judge{\Delta;\Gamma}{e}{A \to B}}; \interp{\judge{\Delta;\Gamma}{e'}{A}}\right\rangle ; \mathrm{eval} \\[1em] \interp{\judge{\Delta;\Gamma}{\val{e}}{F(A)}} = \\ \qquad \sigma_{\Delta,\Gamma}; F(\interp{\judge{\cdot; \Delta,\Gamma}{e}{A}}) \\ \interp{\judge{\Delta;\Gamma}{\letv{\val{x}}{e}{e'}}{C}} = \\ \qquad \left\langle \interp{\judge{\Delta;\Gamma}{e}{F(A)}}; F(\Delta) \times \Gamma\right\rangle ; (\phi_{A, \Delta} \times \Gamma); \interp{\judge{x:A, \Delta; \Gamma}{e'}{C}} \end{array} $$

This is obviously a sound interpretation (modulo typos in my clauses). To close the loop on this post, we would need to construct a cartesian closed category with a strong lax monoidal endofunctor from the term model of the syntax. Again -- future post!

Obviously, some examples would also be nice! The coolest one I know is the application to linearly-typed programming, where we can use applicatives to explain exactly why substructural types make reasoning about imperative programs a lot easier. But that's a post for another day!