ezyang’s blog

the arc of software bends towards understanding

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.

13 Responses to “Applicative functors”

  1. Brent Yorgey says:
    August 16, 2012 at 7:32 am

    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:
    August 16, 2012 at 4:45 pm

    Answers to the exercises (spoiler alert!): https://gist.github.com/3373487

  3. Derek Elkins says:
    August 16, 2012 at 7:33 pm

    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. Edward Z. Yang says:
    August 16, 2012 at 8:22 pm

    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:
    August 19, 2012 at 2:14 pm

    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:
    August 21, 2012 at 8:57 am

    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: http://tomasp.net/blog/applicative-functors.aspx

  7. Frank Atanassow says:
    August 23, 2012 at 6:09 am

    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:
    August 23, 2012 at 9:52 pm

    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:
    April 27, 2014 at 3:18 pm

    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:
    January 16, 2015 at 4:46 am

    > 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. Graphs à la carte | no time says:
    December 12, 2016 at 8:29 pm

    […] 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 […]

  12. Fylwind says:
    April 10, 2017 at 1:05 am

    > The procedure for transformation is kind of neat, I wonder if someone has coded it up.

    Isn’t that what Control.Applicative.Free does? It looks like the `Ap f a` data type is in canonical form:

    > Pure ∷ a → Ap f a
    > Ap ∷ f a → Ap f (a → b) → Ap f b

    For some reason, the ordering of Ap constructor is backward, but if we define `RAp = flip Ap`, then there is a correspondence between Brent’s canonical form and the free applicative:

    > ((pure f ⊛ u1) ⊛ u2) ⊛ u3 …

    > ((Pure f `RAp` u1) `RAp` u2) `RAp` u3 …

  13. Nadrieril says:
    June 22, 2017 at 6:42 pm

    There’s another formulation of applicatives that I have found, but I’m not sure if it actually holds:

    f is Applicative iff arrows of the form `f(a -> b)` form a category.

    There’s a nice similarity with the definition of monads and comonads via kleisli and cokleisli categories.

    I can define instances that typecheck but I’m having trouble proving laws. I think it needs something stronger than Category but I don’t know what.

    data AppArrow f a b = AA (f (a -> b))

    instance Applicative f => Category (AppArrow f) where
    id = AA (pure id)
    (AA f) . (AA g) = AA ((.) f g)

    instance (Functor f, Category (AppArrow f)) => Applicative f where
    pure x = fmap ($ x) id_AA
    ff fx = fmap ($ ()) (ff ._AA fmap const fx)
    where id_AA and ._AA are the id and composition obtained by wrapping/unwrapping the AppArrow category

    I’m posting this here in case someone finds it interesting or wrong.

Leave a Comment