Matthew Chan

← back

A guide to notation in Functional Programming with Bananas, Lenses, and Barbed Wire

27 August 2017

\newcommand{&&&}{;;} \newcommand{***}{;|;} \newcommand{+++}{;|;} \newcommand{|||}{;;}

The difficulty of Meijer et al’s classic paper mostly concerns the liberal introduction of new symbols that are hard to parse and remember. In the interest of making it more comprehensible to myself, I translated the bulk of the definitions and laws to their Haskell equivalents, discovering on the way that they have already been codified as the laws for the Functor, Bifunctor, Profunctor, and Arrow classes.

I hope to translate the rest of the paper sometime, but for now here’s section 3.

Note: I later found that Edward Yang had written a similar translation many years prior, albeit not using some of the canonical typeclasses.

Section 3: Algbraic Data Types


As the paper is really dealing with an idealised functional language rooted in category theory, one must keep in mind the convention in category theory to use the same symbol for the action of the functor on both “terms” (objects) and “types” (categories).

Bifunctors and Monofunctors as described in the paper are different names for the typeclasses Bifunctor and Functor, where the type level operation is the higher kinded type itself and the term level operation is the method that characterises the typeclass.

For example, a Bifunctor \(\dagger\) is characterised by its action on both types and terms, where its action on types (in the GADT style) is \(\dagger \;:\;A \rightarrow B \rightarrow A \dagger B\) and on terms \(\dagger \;:\;(A \rightarrow B) \rightarrow(C \rightarrow D) \rightarrow A\dagger C \rightarrow B\dagger D\), satisfying the usual identity and distributivity laws.

In Haskell, \(\dagger\) is a type of kind * -> * -> * with a bimap:

\[\begin{aligned} id \dagger id &= id \\ f \dagger g \circ h \dagger j &= (f \circ h) \dagger (g \circ j) \end{aligned}\]

The treatment of monofunctors \(F\) is similar, with the action of \(\cdot_F\) on values given by fmap.

Products and sums


Something that I never made the connection with before is that if you look at the definitions from the Control.Arrow class, it is clear that

(***) :: Arrow a       => a b c -> a b' c' -> a (b, b')       (c, c')
(+++) :: ArrowChoice a => a b c -> a b' c' -> a (Either b b') (Either c c')

are just functors to the product and sum categories.

The various familiar term level functions for products and sums are written as


The Arrow functor presented in the paper is in fact the Profunctor instance for (->) in Haskell:

\(\begin{aligned} (f \rightarrow g)\; h = g \circ h \circ f\\ (f \leftarrow_F g)\; h = f \circ h_F \circ g \end{aligned}\)

The second \(\leftarrow_F\) operates on a homomorphically lifted \(h_F\), i.e. dimap f g . fmap.

Of course, dimap distributes over composition:

dimap f g . dimap h j = dimap (h.f) (g.j)

Lifting of functors

For monofunctors \(F,G\) and a bifunctor \(\dagger\), the monofunctors \(FG\) and \(F\dagger G\) are defined by

\(\begin{aligned} \tau_{(FG)} &= (\chi_F)_G \\ \tau_{(F\dagger G)} &= \chi_F \dagger \chi_G \end{aligned}\)

where \(\tau\) is a type of kind \(* \rightarrow*\) and \(\chi\) is a function of type \(a \rightarrow b\). (The left hand side is a type, and the right hand side is a term.)

In Haskell:

fmap . fmap
     :: (Functor f, Functor g)
     => (a -> b) -> (g (f a) -> g (f b))
\f -> bimap (fmap f) (fmap f)
     :: (Functor f, Functor g, Bifunctor p)
     => (a -> b) -> (p (f a) (g a) -> p (f b) (g b))

Laws for the basic combinators

Translated literally,

\(\begin{aligned} \grave{\pi}\circ f \| g &= f \circ \grave{\pi}\\ \acute{\pi}\circ f \*** g &= g \circ \acute{\pi}\\ \grave{\pi}\circ f \&&& g &= f \\ \acute{\pi}\circ f \&&& g &= g \\ (\grave{\pi}\circ h) \&&& (\acute{\pi}\circ h) &= h \\ \grave{\pi}\&&& \acute{\pi}&= id \\ f \*** g \circ h \&&& j &= (f \circ h) \&&& (g \circ j) \\ f \&&& g \circ h &= (f \circ h) \&&& (g \circ h) \\ f \*** g = h \*** j &\equiv f = g \land h = j \\ f \&&& g = h \&&& j &\equiv f = g \land h = j \\ f \+++ g \circ \grave{\iota}&= f \\ f \+++ g \circ \acute{\iota}&= g \\ f \||| g \circ \grave{\iota}&= \grave{\iota}\circ f \\ f \||| g \circ \acute{\iota}&= \acute{\iota}\circ g \\ (h \circ \grave{\iota}) \+++ (h \circ \acute{\iota}) &= h && \text {(h strict) } \\ \grave{\iota}\||| \acute{\iota}&= id \\ (f \||| g) \circ (h \+++ j) &= (f \circ h) \||| (g \circ j) \\ f \circ g \||| h &= (f \circ g) \||| (f \circ h) && \text {(f strict) } \\ f \+++ g = h \+++ j &\equiv f = h \land g = j \\ f \||| g = h \||| j &\equiv f = h \land g = j \end{aligned}\)

The Abides law, in three forms:

\(\begin{aligned} (f \&&& g) \||| (h \&&& j) &= (f \||| h) \&&& (g \||| j)\\ \texttt{(f &&& g) ||| (h &&& j)} &= \texttt{(f ||| h) &&& (g ||| j)}\\ \end{aligned}\)

Logically, it is the tautology: \((f \land g) \lor (h \land j) = (f \lor h) \land (g \lor j)\)

It would seem that the arrow combinators (&&&) and (|||) with product/sum types is isomorphic to the boolean semiring.


part : (a -> Bool) -> a -> Either a a
part p a | p a       = Left a
       | otherwise = Right a

with laws

void . f = void
part p . f = f +++ f . part (p . f)