# Applicative Archery

*July 6, 2015*

It is widely agreed that the laws of the `Applicative`

class are not pretty to look at.

```
pure id <*> v = v -- identity
pure f <*> pure x = pure (f x) -- homomorphism
u <*> pure y = pure ($ y) <*> u -- interchange
pure (.) <*> u <*> v <*> w = u <*> (v <*> w) -- composition
```

Monad laws, in comparison, not only look less odd to begin with but can also be stated in a much more elegant way in terms of Kleisli composition `(<=<)`

. Shouldn’t there be an analogous nice presentation for `Applicative`

as well? That became a static question in my mind while I was studying applicative functors many moons ago. After finding surprisingly little commentary on this issue, I decided to try figuring it out by myself. ^{1}

Let’s cast our eye over `Applicative`

:

If our inspiration for reformulating `Applicative`

is Kleisli composition, the only sensible plan is to look for a category in which the `t (a -> b)`

functions-in-a-context from the type of `(<*>)`

are the arrows, just like `a -> t b`

functions are arrows in a Kleisli category. Here is one way to state that plan in Haskell terms:

```
class Applicative t => Starry t where
idA :: t (a -> a)
(.*) :: t (b -> c) -> t (a -> b) -> t (a -> c)
infixl 4 .*
-- The Applicative constraint is wishful thinking:
-- When you wish upon a star...
```

The laws of `Starry`

are the category laws for the `t (a -> b)`

arrows:

```
idA .* v = v -- left identity
u .* idA = u -- right identity
u .* v .* w = u .* (v .* w) -- associativity
```

The question, then, is whether it is possible to reconstruct `Applicative`

and its laws from `Starry`

. The answer is a resounding yes! The proof is in this manuscript, which I have not transcribed here as it is a little too long for a leisurely post like this one ^{2}. The argument is set in motion by establishing that `pure`

is an arrow mapping of a functor from **Hask** to a `Starry`

category, and that both `(<*>)`

and `(.*)`

are arrow mappings of functors in the opposite direction. That leads to several naturality properties of those functors, from which the `Applicative`

laws can be obtained. Along the way, we also get definitions for the `Starry`

methods in terms of the `Applicative`

ones…

… and vice-versa:

Also interesting is how the property relating `fmap`

and `(<*>)`

…

… now tells us that a `Functor`

results from composing the `pure`

functor with the `(<*>)`

functor. That becomes more transparent if we write it point-free:

In order to ensure `Starry`

is equivalent to `Applicative`

we still need to prove the converse, that is, obtain the `Starry`

laws from the `Applicative`

laws plus the definitions of `idA`

and `(.*)`

just above. That is not difficult; all it takes is substituting the definitions in the `Starry`

laws and:

For left identity, noticing that

`(id .) = id`

.For right identity, applying the interchange law and noticing that

`($ id) . (.)`

is`id`

in a better disguise.For associativity, using the laws to move all

`(.)`

to the left of the`(<*>)`

and then verifying that the resulting messes of dots in both sides are equivalent.

As a tiny example, here is the `Starry`

instance of `Maybe`

…

… and the verification of the laws for it:

```
-- Left identity:
idA .* u = u
Just id .* u = u
-- u = Nothing
Just id .* Nothing = Nothing
Nothing = Nothing
-- u = Just f
Just id .* Just f = Just f
Just (id . f) = Just f
Just f = Just f
-- Right identity:
u .* idA = u
u .* Just id = u
-- u = Nothing
Nothing .* Just id = Nothing
Nothing = Nothing
-- u = Just g
Just g .* Just id = Just g
Just (g .* id) = Just g
Just g = Just g
-- Associativity:
u .* v .* w = u .* (v .* w)
-- If any of u, v and w are Nothing, both sides will be Nothing.
Just h .* Just g .* Just f = Just h .* (Just g .* Just f)
Just (h . g) .* Just f = Just h .* (Just (g . f))
Just (h . g . f) = Just (h . (g . f))
Just (h . g . f) = Just (h . g . f)
```

It works just as intended:

```
GHCi> Just (2*) .* Just (subtract 3) .* Just (*4) <*> Just 5
Just 34
GHCi> Just (2*) .* Nothing .* Just (*4) <*> Just 5
Nothing
```

I do not think there will be many opportunities to use the `Starry`

methods in practice. We are comfortable enough with applicative style, through which we see most `t (a -> b)`

arrows as intermediates generated on demand, rather than truly meaningful values. Furthermore, the `Starry`

laws are not really easier to prove (though they are certainly easier to remember!). Still, it was an interesting exercise to do, and it eases my mind to know that there is a neat presentation of the `Applicative`

laws that I can relate to.

This post is Literate Haskell, in case you wish to play with `Starry`

in GHCi (here is the raw .lhs file ).

```
instance Starry Maybe where
instance Starry [] where
instance Starry ((->) a) where
instance Starry IO where
```

As for proper implementations in libraries, the closest I found was `Data.Semigroupoid.Static`

, which lives in Edward Kmett’s `semigroupoids`

package. *“Static arrows”* is the actual technical term for the `t (a -> b)`

arrows. The module provides…

… which uses the definitions shown here for `idA`

and `(.*)`

as `id`

and `(.)`

of its `Category`

instance.

There is a reasonably well-known alternative formulation of

`Applicative`

: the`Monoidal`

class as featured in this post by Edward Z. Yang. It is quite handy to work with when it comes to checking whether an instance follows the laws.↩Please excuse some oddities in the manuscript, such as off-kilter terminology and weird conventions (e.g. consistently naming arguments in applicative style as

`w <*> v <*> u`

rather than`u <*> v <*> w`

in applicative style). The most baffling choice was using`id`

rather than`()`

as the throwaway argument to`const`

. I guess I did that because`($ ())`

looks bad in handwriting.↩

Post licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.