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.
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:
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.
Obviously,
(,)Either.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}\)
instance Profunctor (->) where
dimap f g h = g . h . fThe 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)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))\(\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 = jThe 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.
part : (a -> Bool) -> a -> Either a a
part p a | p a = Left a
| otherwise = Right awith laws
void . f = void
part p . f = f +++ f . part (p . f)