← back

Functional Programming with Bananas, Lenses, and Barbed Wire in Haskell, part 1

27 August 2017

The hardest bit about Meijer et al's classic paper is all the weird symbols introduced just before things get interesting, symbols that don't map to an intuition from modern Haskell. (I never made it past section two.) Today I finally sat down and worked my way through the symbols, translating the definitions into Haskell as I went, and realised that all that the section describes are just 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

Functors

Perhaps the most confusing thing about the paper's presentation of functors is that the same symbol is used to stand for both a term and type level function, which makes sense from a category theory perspective but is strange from a programming perspective.

Bifunctors and Monofunctors as described here are just 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}\]
class Bifunctor (†) a c where
  bimap :: (a -> b) -> (c -> d)
        -> a † c -> b † d

bimap id id = id
bimap f g . bimap h j = bimap (f . h) (g . j)

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

Products and sums

Obviously,

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

Arrow

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}\)

instance Profunctor (->) where
  dimap f g h = g . h . f

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

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

fst . f *** g = f . fst
snd . f *** g = g . snd
fst . f &&& g = f
snd . f &&& g = g
(fst . h) &&& (snd . h) = h
fst &&& snd = id
f *** g . h &&& j = (f . h) &&& (g . j)
f &&& g . h = (f . h) &&& (g . h)
f *** g = h *** j <=> f = g AND h = j
f &&& g = h &&& j <=> f = g AND h = j
f +++ g . Left = f
f +++ g . Right = g
f ||| g . Left = Left . f
f ||| g . Right = Right . g
(h . Left) +++ (h . Right) = h (h strict)
Left ||| Right = id
(f ||| g) . (h +++ j) = (f . h) ||| (g . j)
f . g ||| h = (f . g) ||| (f . h)  (f strict)
f +++ g = h +++ j <=> f = h AND g = j
f ||| g = h ||| j <=> f = h AND g = j

The Abides law, in three forms:

\(\begin{aligned} (f {\;\triangle\;}g) {\;\triangledown\;}(h {\;\triangle\;}j) &= (f {\;\triangledown\;}h) {\;\triangle\;}(g {\;\triangledown\;}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.

Varia

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)