Inside 214-1E

Existential Pontification and Generalized Abstract Digressions

Applicative functors

On the importance of primary sources.

(Introductory material ahead.) Most readers of this blog should have at least a passing familiarity with applicative functors:

class Applicative f where
  pure :: a -> f a
  (<*>) :: f (a -> b) -> f a -> f b

This interface is quite convenient for day-to-day programming (in particular, it makes for the nice f <$> a <*> b <*> c idiom), but the laws it obeys are quite atrocious:

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

So, if you (like me twenty-four hours ago) haven’t seen it already, you should show that this interface is equivalent to Applicative:

class Functor f => Monoidal f where
  unit :: f ()
  (**) :: f a -> f b -> f (a,b)

(By the way, if you haven’t shown that join :: m (m a) -> m a for monads is equivalent to bind :: m a -> (a -> m b) -> m b, you should do that too.) The laws for this formulation are much nicer:

    [naturality] fmap (f *** g) (u ** v) = fmap f u ** fmap g v
 [left identity] unit ** v ≅ v
[right identity] u ** unit ≅ u
 [associativity] u ** (v ** w) ≅ (u ** v) ** w

Where f *** g = \(x,y) -> (f x, g y). I’ve prettied things up a bit by using “is isomorphic to” in order to suppress the differences between ((), a) and a, as well as (a,(b,c)) and ((a,b),c), for strict equalities you’ll need some extra functions to massage the results into the right types. It seems that there is a general pattern where the API which has nice formulations of laws is not convenient to program with, and the formulation which is nice to program with does not have nice laws. C’est la vie... but at least they’re equivalent!

With this formulation, it becomes trivial to state what laws commutative applicative functors obey:

[commutativity] u ** v ≅ v ** u

The original paper Applicative Programming With Effects is well worth a read. Check it out! That concludes this public service announcement.

11 Responses to “Applicative functors”

  1. Brent Yorgey says:

    Cool, thanks! I knew about the alternative presentation in terms of Monoidal, but had never actually seen/paid attention to the alternative presentation of the laws. Much nicer indeed. I may have to go stick that in the Typeclassopedia…

    Note that there is a semi-nice way to interpret the usual Applicative laws, in that they give a procedure for transforming any Applicative expression into a canonical form with exactly one call to ‘pure’ at the beginning, followed by a left-nested chain of ‘s. Though that doesn’t help with the intuition as to WHY these laws should hold.

  2. Mikhail Glushenkov says:

    Answers to the exercises (spoiler alert!):

  3. Derek Elkins says:

    The second presentation is a witness to the fact that applicative functors are lax monoidal functors, as the second presentation directly lines up with the typical presentation of lax monoidal functors.

  4. Brent: Yeah, I think they deserve a mention, much the same way the alternate formulation of bind with ‘join’ deserves a mention. The procedure for transformation is kind of neat, I wonder if someone has coded it up.

    Derek: I avoided mentioning them because I… don’t really know what a lax monoidal functor is. ;-)

  5. Derek Elkins says:

    A category is a monoidal category if it has a monoidal product, ⊗, that is associative and has a unit I (up to isomorphism). A functor is monoidal if it preserves the monoidal structure up to isomorphism, i.e. FI ≅ I and F(A⊗B) ≅ FA⊗FB plus preserving the arrows witnessing associativity and the left/right unit laws. A functor is lax monoidal if instead of an isomorphism you simply have a natural transformation (going from right to left using the above isomorphisms) and it’s oplax monoidal if you have a natural transformation going the other way.

    Identifying () with I, (,) with ⊗ and writing unit :: () -> f () and (**) :: (f a, f b) -> f (a,b) [another name for unit and (**) could be liftA0 and liftA2].

  6. Tomas Petricek says:

    I always liked the ‘Monoidal’ definition of applicative functors better than the ‘Applicative’ definition. I suppose that’s because I look at it from a different perspective. I’m not a reguler Haskell programmer (where the applicative style is very useful), but an ML/F# programmer (where the other view seems more useful to me – in fact, I even created a simple syntactic extension for using ‘Monoidal’ computations in F# that is related to the syntax for monads in an interesting way).

    I failed to describe that in a brief comment, so here is a longer reply as a blog post:

  7. Frank Atanassow says:

    Lax monoidal functors are a bit more general than applicative functors on the same category. Applicative functors are lax monoidal functors for the monoidal fragment of the cartesian structure on a category, that is, for the tensor product given by the cartesian product. In general, a monoidal functor could use a different monoidal structure, for example the co-cartesian one.

    The fact that the laws for applicative functors look ugly while the laws for the lax monoidal presentation look intuitive suggests to me that our term syntax is not optimal because it is stuck in an old paradigm. Hmm.

  8. Pseudonym says:

    One other observation. The only “law” for Monoidal which has an equals sign rather than a congruence isn’t a “law” in the sense that it’s a burden that someone writing a Monoidal instance has to prove. It’s just the free theorem for (**).

    Compare this with the free theorem for (), which has a naturality precondition that seems very hard to work with:

    (forall h k. g . k = h k . f
    fmap h p = y)
    fmap g (p q) = y fmap f q

  9. Michael Baker says:

    Would you mind explaining the statement “but the laws it obeys are quite atrocious”? I don’t have the context that allows me to know what makes a law nice and what makes it ugly, but you seem to have some specific feelings about what makes a good law.

  10. Paolo G. Giarrusso says:

    > It seems that there is a general pattern where the API which has nice formulations of laws is not convenient to program with, and the formulation which is nice to program with does not have nice laws.

    That might be because we seem to define “nice laws” as “ones we’re familiar with from algebra”, and algebra does not have binders — at best, you have combinatory logic or CCCs, where you encode variables somehow, but where few like to program.

    However, monads do have a nice non-standard formulation (with `>=>`) which is almost natural — but you’d need to encode values `v: V` with functions from `Unit -> V`, like global elements in category theory.

  11. […] side note: the type signature of box reminds me of this blog post by Edward Yang and makes me wonder if Functor, Foldable plus idempotent and commutative Monoid […]

Leave a Comment