What is the mathematical name for Haskell's Alternative Functor

Question

Haskell's Applicative Functor is called Lax Monoidal Functor in mathematics.

What is Haskell's Alternative Functor called in mathematics?

Recall that Haskell's Alternative Functor is defined as follows:

class Applicative f => Alternative f where
    -- | The identity of '<|>'
    empty :: f a
    -- | An associative binary operation
    (<|>) :: f a -> f a -> f a

Edit: In other words, an Alternative Functor f is an Applicative Functor such that for every type a, f a is a monoid, where <|> is the binary operation of type f a -> f a -> f a and empty is the identity of type f a. Uncurrying the type of <|>, we get $$f\ a \times f\ a \rightarrow f\ a$$ and empty can be equivalently defined to have type $$1 \rightarrow f\ a$$ In the Haskell definition, the type variable a is universally quantified. As far as I know, this translates to the requirement that they are natural in a.

Answer 1

This is not a complete answer, just a translation of Haskell to math so that the resident category theorists can tell what the question is.

As is usual in such cases, the terminology and the concepts in Haskell are slightly modified concepts from mathematics. It is best in the first iteration to look just at the broad similarities and not worry so much about the details.

Recall from Section 7 of the paper by Connor McBride and Ross Paterson that Haskell's Applicative is a lax monoidal functor (kind of as the Haskell definition uses internal Hom-sets where one would expect the external ones).

The definition of Alternative translates into: a functor $F : \mathcal{C} \to \mathcal{C}$, where $C$ is at least cartesian, together with natural transformations $e : 1 \to F$ and $m : F({-}) \times F({-}) \to F$, or concretely, for every object $A \in \mathcal{C}$ we have arrows $$e_A : 1 \to F(A)$$ and $$m_A : F(A) \times F(A) \to F(A)$$ such that $(F(A), e_A, m_A)$ is a monoid for all $A$, naturally in $A$. What would you call such a thing?

The next question to ask is whether there is anything extra about having a lax monoidal functor which also has the above structure of monoids? I don't know off the top of my head. If there is another view of the same situation, it will surely be useful for various Haskell hacking tricks. Haskell people are very good at using category-theoretic algebra for all sorts of cool purposes.

Let me also explain on the difference between parametricity and naturality. When we define a "functor" $F$ in Haskell, that is not really a functor. It is acertain mapping from types to types which acts on internal hom-sets as a functor would. In addition, this mapping has a strong property known as parametricity which says that $F$ behaves "in the same way" on all types. Parametricity is quite similar to naturality, and there is a way to view it semantically as such, but it is not precisely naturality. This is not a detail into which we should worry about here, though.

Answer 2

A slightly different set of primitive operations that we can look at is the following:

class Functor f => Alternative' f
  where
  unit :: () -> f Void
  zip :: (f a, f b) -> f (Either a b)

This represents a lax monoidal functor from the monoidal category of -> under the tensor Either to the monoidal category of -> under the tensor (,). The laws are the usual laws for the coherence maps of lax monoidal functors, including those that demand conformance with the functor (i.e. you can crib them with minor adjustments from the Applicative typeclass).

By contrast, the operations and laws of the Alternative typeclass of today seem to amount to type Alternative f = Monoid (forall a. f a). We can witness a pair of maps that convert between the primitive operations of Alternative' and Alternative:

instance Alternative f => Alternative' f
  where
  unit _ = empty
  zip (fa, fb) = (Left <$> fa) <|> (Right <$> fb)

instance Alternative' f => Alternative f
  where
  empty = absurd <$> unit ()
  fa1 <|> fa2 = either id id <$> zip (fa1, fa2)

However, it seems likely that this is not truly an isomorphism, due to the difference in constraints and laws between the two typeclasses.

On one hand, Alternative is more permissive than Alternative', since it does not demand any form of compatibility between the monoid and the functor, whereas the commutative diagrams of a lax monoidal functor do.

On, the other hand, Alternative demands Applicative, a constraint that Alternative' does not demand. When viewed through the lens of lax monoidal functors, Applicative f simply means that f coheres the (,) monoidal structure to (,), and Alternative f means that it coheres the Either monoidal structure to (,). These are orthogonal claims, so there is no need for Alternative' f to demand a Applicative f constraint.

That said, I conjecture that most types that support Alternative instances also support a lawful instance of Alternative', and so you can imagine them to be "applicatives for different tensor".

Answer 3

This might not be the right approach, but here's my take on the question:

If $(\mathcal{C}, \otimes, I, \dots)$ is a (strict, for the sake of readability) monoidal category, we can endow $[\mathcal{C}, \mathcal{C}]$ with two different monoidal structures:

1. The "usual" monoidal structure, where $\circ$ is the product and $\mathbf{1}_\mathcal{C}$ is the unit. This is the monoidal category whose monoids are called monads. Notice how this doesn't actually use the fact that $\mathcal{C}$ is endowed with a monoidal structure.

2. The "other" (I sometimes refer to it as "pointwise") monoidal structure has "pointwise $\otimes$" (let's call it $\boxtimes$) as product, and $\Delta_I$ (the constant functor on the unit object of $\mathcal{C}$) as monoidal units. In this category, monoids are related to what Haskell programmers call "alternative" functors, but without the part about being "applicative" and with one additional property. This can be further generalized to the case of functors $\mathcal{B} \to \mathcal{C}$ where $\mathcal{B}$ is not required to be monoidal, and everything that follows should work just fine (but I won't venture there).

Let me elaborate on the latter, since the former is (probably) already well-known to most haskell programmers here (other than being significantly less relevant):

First we'll need to properly define $\boxtimes$: if we fix functors $\mathcal{F}, \mathcal{G} : \mathcal{C} \to \mathcal{C}$ we can define $(\mathcal{F} \boxtimes \mathcal{G}) (a) := \mathcal{F}(a) \otimes \mathcal{G}(a)$ (the definition for morphisms is analogous). This, together with $\Delta_I$ as a unit, defines a monoidal category: all axioms (and further properties, such as symmetry and strictness) follow trivially from the monoidal structure on $\mathcal{C}$.

Now, monoids in this monoidal category are what haskell programmers call "alternative" functors, but that's not all: they are so in a functorial way, meaning that if $f : a \to b : \mathcal{C}$ and $\mathcal{M}$ is a monoid in $([\mathcal{C}, \mathcal{C}], \boxtimes, \Delta_I)$ then $\mathcal{M}(f)$ is a morphism of monoids. To see this, note how this diagram needs to commute in a pointwise fashion, and the same applies to this other diagram too. We're in the strict case, but nothing significant changes in the general one (except that you need to keep track of the coherence laws).

A more abstract (but equivalent) formulation is that each object $\mathcal{M} : \mathbf{Mon}([\mathcal{C}, \mathcal{C}])$ naturally defines a functor $\hat{\mathcal{M}} : \mathcal{C} \to \mathbf{Mon}(\mathcal{C})$, and this point of view leads to the observation that this actually defines a functor $(\hat{-}) : \mathbf{Mon}([\mathcal{C}, \mathcal{C}]) \to [\mathcal{C}, \mathbf{Mon}(\mathcal{C})]$.

What this amounts to is just that a "monoidal" natural transformation $\nu : \mathcal{M} \to \mathcal{N} : \mathbf{Mon}([\mathcal{C}, \mathcal{C}])$ between monoid object in this "pointwise" monoidal category of (endo)functors also defines a natural transformation $\hat{\nu} : \hat{\mathcal{M}} \to \hat{\mathcal{N}} : [\mathcal{C}, \mathbf{Mon}(\mathcal{C})]$: the argument is similar but you need to look at the diagrams for morphisms of monoids.

Things are not over yet: it seems that $(\hat{-})$ is actually an equivalence of categories! You can convince yourself of this if you squint hard enough, and the argument is roughly "brute force":

Let's construct a strict inverse to $(\hat{-})$, call it $(\tilde{-})$: take $\mathcal{F} : \mathcal{C} \to \mathbf{Mon}(\mathcal{C})$, compose it with the forgetful functor $\mathbf{U} : \mathbf{Mon}(\mathcal{C}) \to \mathcal{C}$. We'll now use the "forgotten structure" on $\mathcal{F}$ to endow $\mathbf{U} \circ \mathcal{F}$ with the structure of a monoid in $[\mathcal{C}, \mathcal{C}]$: to do this, notice how the monoid structure on $\mathcal{F}(a)$ (for $a : \mathcal{C}$) needs to be such that each morphism $\mathcal{F}(f) : \mathcal{F}(a) \to \mathcal{F}(b)$ is a morphism of monoids: this amounts to saying that the correspondences $a \mapsto \mathbf{m}^{\mathcal{F}(a)}$ and $a \mapsto \mathbf{e}^{\mathcal{F}(a)}$ are natural in $a$ and hence natural transformations (its now trivial to check that these endow $\mathbf{U} \circ \mathcal{F}$ with the structure of a monoid in $[\mathcal{C}, \mathcal{C}]$).

We now need to check that $(\hat{-}) \circ (\tilde{-}) = \mathbf{1}_{[\mathcal{C}, \mathbf{Mon}(\mathcal{C})]}$ and $(\tilde{-} \circ \hat{-}) = \mathbf{1}_{\mathbf{Mon}([\mathcal{C}, \mathcal{C}])}$: they should both be long and trivial computations, and I'll (boldly) omit them.

Edit: this can probably be "merged" to the other answer by Andrej Bauer to give a more complete answer