eighty-twenty

Yesterday, I became inspired to learn about the kinds of generalized, pure-functional getters and setters that the FP community calls “optics”: Lenses, Prisms, Folds, Traversals, and so on.

I quickly realised that I needed to brush up on some of the core typeclasses involved, namely Functor and Applicative. I spent the rest of the day reading up on the laws and definitions involved.

Brent Yorgey’s Typeclassopedia and Miran Lipovača’s Learn You A Haskell were both great starting points. The latter for the basics, some good examples, and lots of context-setting and motivation, and the former for completeness, concision, and connections to the other foundational ideas in the Haskell standard library.

Applicative laws vs. Monoidal laws

The laws for Applicative functors are complicated, and have obscure, largely unhelpful¹ names like “homomorphism” and “interchange”.

The laws for Monoidal functors are simple and familiar: just left and right identity, and an associativity law.

However, each set of laws implies the other!

The two formulations are equivalent. I spent most of yesterday evening proving this, as suggested by the exercises in the Typeclassopedia section dealing with Monoidal functors.

The main thing I learned from this exercise is that the Applicative laws are self-contained. They imply the Functor laws, the Monoidal laws, and the “naturality” law all by themselves. By contrast, the Monoidal laws are not self-contained: in order to derive the Applicative laws, you need appeal to the Functor and “naturality” laws from time to time.

On the one hand, the Applicative laws are ugly, but self-contained. On the other hand, the Monoidal laws are cleanly factored and separate from the Functor laws. But on the gripping hand, programming with Applicative is reported to be much less of a pain than programming with Monoidal. I believe it!

All this suggests that choosing the Applicative formulation over the Monoidal one makes sense when designing a language’s standard library.

After all, proving that an instance of Applicative respects the laws can be done either in terms of the Applicative laws or the Functor+Monoidal laws, meaning that not only does the programmer have the better API, but the implementor has a free choice of “proof API” when discharging their proof obligations.

A handy lemma

Another result of working through the proofs was discovery of this handy lemma:

pure f <*> u <*> pure h = pure (flip f) <*> pure h <*> u

It’s intuitively obvious, and something that I think many users of Applicative will rely on, but it took a bit of thinking to realise I needed it, and a little more thinking to get the proof to go through.

(Exercise: Imagine replacing pure h with v. Why does the new statement not hold?)

Onward to Foldable, Traversable, Lens and Prism

I think today I’ll read the rest of the Typeclassopedia, with particular focus on Foldable and Traversable. If I have time, I’ll get started on Lens.