Applicative Functor

On a closed monoidal category the applicative and lax monoidal enrichments of a functor are the same structure, since applying a wrapped function to a wrapped argument coincides with merging two wrapped values; a strength is a third, weaker enrichment.

Fix a closed monoidal category and an endofunctor . Three structures enrich beyond functoriality:

• a strong functor has a strength that pulls a pure factor inside;
• an applicative functor has and, for all , an application map ;
• a lax monoidal functor has a unit and a coherence .

is the running example. Here is the singleton, applies every wrapped function to every wrapped argument, and is the cartesian-product zip.

Proposition. Applicative equals lax monoidal

On a closed monoidal category the applicative and lax monoidal structures on are interdefinable. From one recovers application as , which combines the wrapped function with its wrapped argument and then applies evaluation under . Conversely is the lax unit transposed. The two packages of data determine each other, so “applicative functor” and “lax monoidal functor” name the same structure.

References

• McBride & Paterson, ‘Applicative Programming with Effects’, Journal of Functional Programming (2008)
• Rivas & Jaskelioff, ‘Notions of Computation as Monoids’ (2017)