Equivalence of Applicative Functors and Multifunctors
Andreas Abel
TL;DR
This work proves the equivalence between Applicative functors and Multifunctors by showing that the familiar applicative laws can be captured by a single, uniform family of lift operations $\mathsf{liftA}_{n}$. It demonstrates two directions: (i) multifunctors induce an applicative structure via $u\,\_⊛\, v = \mathsf{liftA}_{2}\,\mathsf{id}\,u\,v$, and (ii) applicative functors induce a full multifunctor through recursive definitions $\mathsf{liftA}_{0} x = \mathsf{pure} \, x$ and $\mathsf{liftA}_{n+1} f \vec{u} v = \mathsf{liftA}_{n} f \vec{u} \_⊛\; v$, with a composition law proved by induction. The core result is that a small, compositional set of liftA laws subsumes the standard four applicative laws, unifying the theory and clarifying the algebra of effectful computations under category-theoretic notions of multifunctors and lax monoidal functors.
Abstract
McBride and Paterson introduced Applicative functors to Haskell, which are equivalent to the lax monoidal functors (with strength) of category theory. Applicative functors F are presented via idiomatic application $\_\circledast\_ : F (A \to B) \to F A \to F B$ and laws that are a bit hard to remember. Capriotti and Kaposi observed that applicative functors can be conceived as multifunctors, i.e., by a family liftA$_n$ : $(A_1 \to ... \to A_n \to C) \to F A_1 \to ... \to F A_n \to F C$ of zipWith-like functions that generalize pure $(n=0)$, fmap $(n=1)$ and liftA2 $(n=2)$. This reduces the associated laws to just the first functor law and a uniform scheme of second (multi)functor laws, i.e., a composition law for liftA. In this note, we rigorously prove that applicative functors are in fact equivalent to multifunctors, by interderiving their laws.