Equivalence of Applicative Functors and Multifunctors

Andreas Abel

paper

Equivalence of Applicative Functors and Multifunctors

arXiv:2401.14286

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 $_⊛_: 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.

6 pages