Applicative functors
by Edward Z. Yang
(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.
Did you enjoy this post? Please subscribe to my feed!
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.
Answers to the exercises (spoiler alert!): https://gist.github.com/3373487
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.
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. ;-)
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].
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
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.
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