← back

title: "A guide to notation in Functional Programming with Bananas, Lenses, and Barbed Wire" date: 2017-08-27 ---

\usepackage{amsmath}

\newcommand{\fst}{\grave{\pi}} \newcommand{\snd}{\acute{\pi}} \newcommand{\inl}{\grave{\iota}} \newcommand{\inr}{\acute{\iota}}

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

\newcommand{\to}{\rightarrow} \newcommand{\ty}{\;:\;} \newcommand{\cata}[1]{(\kern-0.17em|#1|\kern-0.17em)} \newcommand{\ana}[1]{[\kern-0.17em(#1)\kern-0.17em]}

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

Functors

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 \ty A \to B \to A \dagger B$ and on terms $\dagger \ty (A \to B) \to (C \to D) \to A\dagger C \to B\dagger D$, satisfying the usual identity and distributivity laws.

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

<div class="wide row u-max-full-width u-full-width"> <div class="one-half column u-max-full-width u-full-width"> \begin{aligned} id \dagger id &= id \ f \dagger g \circ h \dagger j &= (f \circ h) \dagger (g \circ j) \end{aligned} </div> <div class="one-half column u-max-full-width u-full-width">

```hs 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) ``` </div> </div>

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

hs (***) :: 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:

<div class="row u-max-full-width u-full-width"> <div class="one-half column u-max-full-width u-full-width">

$\begin{aligned} (f \rightarrow g)\; h = g \circ h \circ f\ (f \leftarrowF g)\; h = f \circ hF \circ g \end{aligned}$

/div>

<div class="one-half column u-max-full-width u-full-width"> hs instance Profunctor (->) where dimap f g h = g . h . f </div> </div>

The second $\leftarrowF$ operates on a homomorphically lifted $hF$, 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)} &= (\chiF)G \ \tau{(F\dagger G)} &= \chiF \dagger \chiG \end{aligned}$

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

In Haskell:

hs 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,

<div class="wide row u-max-full-width u-full-width"> <div class="one-half column u-max-full-width u-full-width">

$\begin{aligned} \fst \circ f \| g &= f \circ \fst \ \snd \circ f *** g &= g \circ \snd \ \fst \circ f \&&& g &= f \ \snd \circ f \&&& g &= g \ (\fst \circ h) \&&& (\snd \circ h) &= h \ \fst \&&& \snd &= 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 \inl &= f \ f +++ g \circ \inr &= g \ f \||| g \circ \inl &= \inl \circ f \ f \||| g \circ \inr &= \inr \circ g \ (h \circ \inl) +++ (h \circ \inr) &= h && \text {(h strict) } \ \inl \||| \inr &= 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}$

/div>

<div class="one-half column u-max-full-width u-full-width">

hs 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 </div> </div>

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.

Varia

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

with laws

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

<!-- a natural transformation is a homomorphism on the functor category

f : a -> b function F,G functors

phi :: forall a. F a -> G a satisfying

phi . fmap f = fmap g . phi

via diagram -->

<!-- FP laws and propositional logic

Exportation (curry) Hypothetical syllogism (composition) Biconditional introduction (isomorphism) Conjunction introduction (pair) / elimination (fst/snd) Disjunction intro (Either) / disjunctive syllogism (exl/exr) D isjunction elimination (|||) Constructive dilemma (+++)

(&&&) :: (a -> b) -> (a -> c) -> a -> (b,c) Absorption (\f -> id &&& f)

(|||) is Data.Either.either -->