## Lenses are the coalgebras for the costate comonad

I took part in the Dagstuhl Seminar on Bidirectional Transformations “BX” earlier this month. It was a meeting of people from four communities—databases, graph transformations, programming languages, and software engineering—discussing their various perspectives—namely the view–update problem in databases, triple graph grammars, lenses, and model synchronization—on the common problem of “BX”.

While there, I reported on a marvellous observation made by Russell O’Connor, that lenses are exactly the coalgebras for the costate comonad. That is, the independently identified notion of a “very well-behaved lens” in the work of Pierce and others coincides exactly with the categorical notion of a “coalgebra” for a particular comonad, the “costate” comonad. I’ll unpack that claim here.

## Lenses

Pierce’s lenses are pairs of functions between “source” and “view” datatypes ${S}$ and ${V}$: a “get” function ${g : S \rightarrow V}$ and a “put” function ${p : S \times V \rightarrow S}$. The story is that the view is some projection of the data in the source—perhaps a subset of the data, or the data in a simpler format—and so in order to update the source given a modified view, one needs also a copy of the original source from which to reconstruct the missing information.

For these two functions to capture a “well-behaved” lens, they should satisfy the so-called Get–Put and Put–Get laws:

$\displaystyle \begin{array}{lcl} p\,(s,g\,s) &=& s \\ g\,(p\,(s,v)) &=& v \end{array}$

The Get–Put law says that if you “get” a view of the source, and then “put” it straight back without modifying it, the source remains unmodified: a no-op edit on the view translates into a no-op on the source. The Put–Get law says that if you “put” any view into a source and then “get” it back, you end up with the view you first thought of: nothing is lost from the view when it is put back.

Additionally, for these two functions to capture a “very well-behaved” lens, they must satisfy a third law, the Put–Put law:

$\displaystyle \begin{array}{lcl} p\,(p\,(s,v),u) &=& p\,(s,u) \end{array}$

In words, “put”ting back two views ${v}$ then ${u}$ is equivalent to “put”ting back just the second; any changes to the source from putting back ${v}$ are completely overwritten when putting back ${u}$. (This turns out to be rather a strong condition, requiring that the source basically factors into the view and a completely independent “complement”; few real applications of bidirectional transformation satisfy it. But that’s another story.)

Intuitively, comonads capture “data in context”. A comonad ${(D,\mathit{extr},\mathit{dupl})}$ consists of a functor ${D}$ together with two natural transformations ${\mathit{extr} : D \rightarrow 1}$ and ${\mathit{dupl} : D \rightarrow DD}$ that extract the data from its context and duplicate the context, satisfying the three axioms:

$\displaystyle \begin{array}{lcl} \mathit{extr} \cdot \mathit{dupl} &=& \mathit{id} \\ \mathit{fmap}\,\mathit{extr} \cdot \mathit{dupl} &=& \mathit{id} \\ \mathit{fmap}\,\mathit{dupl} \cdot \mathit{dupl} &=& \mathit{dupl} \cdot \mathit{dupl} \end{array}$

One example of a comonad is the “costate” construction: for fixed ${V}$, define functor ${D}$ by

$\displaystyle \begin{array}{lcl} D\,A &=& V \times (V \rightarrow A) \end{array}$

so that the “map” function for ${D}$ satisfies ${\mathit{fmap}\,h\,(v,f) = (v, h \cdot f)}$. The operations are given by

$\displaystyle \begin{array}{lcl} \mathit{extr}\,(v,f) &=& f\,v \\ \mathit{dupl}\,(v,f) &=& (v, \lambda u \rightarrow (u,f)) \end{array}$

Verifying that these definitions satisfy the comonad axioms is left as an exercise for the interested reader.

(Incidentally, I think it’s called the “costate” comonad more because it is the dual ${(V\times)\cdot(V\rightarrow)}$ of the “state” monad ${(V\rightarrow)\cdot(V\times)}$, rather than because it has anything to do with stateful computations. However, it does model state in the sense of stored variables; and indeed, Russell O’Connor’s blog posting calls ${D}$ the “store” comonad.)

For a functor ${F}$, an ${F}$-coalgebra is a pair ${(A,f)}$ of a type ${A}$ and a function ${f : A \rightarrow F\,A}$. A “coalgebra for a comonad ${D}$” is a ${D}$-coalgebra that interacts well with the operations ${\mathit{extr}}$ and ${\mathit{dupl}}$ of the comonad; that is, the function ${f}$ should also satisfy the laws:

$\displaystyle \begin{array}{lcl} \mathit{extr} \cdot f &=& \mathit{id} \\ \mathit{dupl} \cdot f &=& \mathit{fmap}\,f \cdot f \end{array}$

(Another incidentally: I don’t have a feeling for what these laws mean, in the way that I do for the laws of an algebra of a monad. At least for the free monads ${T}$ that represent terms with free variables, an algebra is a pair ${(A, f : T\,A \rightarrow A)}$ such that ${f}$ makes sense as an “expression evaluator”—it respects singleton variables and substitution. It’s clear to me that the laws of a coalgebra for a comonad are the obvious duals of those for the algebra of a monad; and that they describe the interesting ways of putting together the coalgebra operation with the comonad operations; but I still don’t have a direct intuition. Any comments gratefully received!)

## Lenses are coalgebras of the costate comonad

Now it’s just a matter of putting the pieces together. Curry the “put” function of a lens to obtain ${p : S \rightarrow (V \rightarrow S)}$, and define a lens to be the fork of the “get” and “put” functions:

$\displaystyle \begin{array}{lcl} \ell\,s &=& (g\,s, p\,s) \end{array}$

Note that now ${\ell : S \rightarrow D\,S}$ where ${D}$ is the costate comonad. The Get–Put law is equivalent to the counit axiom of the coalgebra:

$\displaystyle \begin{array}{ll} & \mathit{extr} \cdot \ell = \mathit{id} \\ \Leftrightarrow & \qquad \{ \mbox{apply to an~} s \} \\ & \mathit{extr}\,(\ell\,s) = s \\ \Leftrightarrow & \qquad \{ \ell \} \\ & \mathit{extr}\,(g\,s, p\,s) = s \\ \Leftrightarrow & \qquad \{ \mathit{extr} \} \\ & p\,s\,(g\,s) = s \end{array}$

And the Put–Get and Put–Put laws together are equivalent to the coassociativity axiom:

$\displaystyle \begin{array}{ll} & \mathit{dupl} \cdot \ell = \mathit{fmap}\,\ell \cdot \ell \\ \Leftrightarrow & \qquad \{ \mbox{apply to an~} s \} \\ & \mathit{dupl}\,(\ell\,s) = \mathit{fmap}\,\ell\,(\ell\,s) \\ \Leftrightarrow & \qquad \{ \ell \} \\ & \mathit{dupl}\,(g\,s, p\,s) = \mathit{fmap}\,\ell\,(g\,s, p\,s) \\ \Leftrightarrow & \qquad \{ \mathit{fmap} \mbox{~for~} D \} \\ & \mathit{dupl}\,(g\,s, p\,s) = (g\,s, \ell \cdot p\,s) \\ \Leftrightarrow & \qquad \{ \mathit{dupl} \} \\ & (g\,s, \lambda v \rightarrow (v, p\,s)) = (g\,s, \ell \cdot p\,s) \\ \Leftrightarrow & \qquad \{ \mbox{first components are clearly equal} \} \\ & \lambda v \rightarrow (v, p\,s) = \ell \cdot p\,s \\ \Leftrightarrow & \qquad \{ \mbox{apply to a~} v \} \\ & (v, p\,s) = \ell\,(p\,s\,v) \\ \Leftrightarrow & \qquad \{ \ell \} \\ & (v, p\,s) = (g\,(p\,s\,v), p\,(p\,s\,v)) \\ \Leftrightarrow & \qquad \{ \mbox{apply second components to a~} u \} \\ & (v, p\,s\,u) = (g\,(p\,s\,v), p\,(p\,s\,v)\,u) \\ \Leftrightarrow & \qquad \{ \mbox{pair equality is pointwise} \} \\ & v = g\,(p\,s\,v) \land p\,s\,u = p\,(p\,s\,v)\,u \end{array}$

Posted in Uncategorized | 6 Comments

I read quite a nice problem on Nick Wu’s blog, which will serve as a fine warm-up exercise. It’s about the fact that streams (infinite lists) form a monad, in a different way from lists. Nick shows the “right” and two “wrong” definitions of the join or bind operation, distinguishing them on the basis of the monad laws. But I think Nick’s proofs are more complicated than they need to be, because he hasn’t fully exploited the recursion patterns that underlie his definitions.

This post will involve some language that we have not yet covered. Fear not! I hope it will be clear from context. But in case it isn’t, you might want to take a look at some of the background material (especially the paper Calculating Functional Programs).

## Streams

Like Nick, for simplicity we will take the datatype of streams to be a synonym for lists; in all that follows, assume that lists are properly infinite (not finite, or partial).

$\displaystyle \mathbf{type}\;\mathit{Stream}\,a = [a]$

Streams are naturally a codatatype rather than a datatype: in the category of sets and total functions, they would be represented as a final coalgebra rather than an initial algebra. In Haskell, which is roughly based on the category of CPOs and continuous functions, initial algebras and final coalgebras coincide, so we need not (indeed, we cannot) make the distinction formally. But we can make it informally, by stipulating that the basic pattern of computation for streams is the ${\mathit{unfold}}$:

$\displaystyle \begin{array}{l} \mathit{unfold} :: (b \rightarrow (a,b)) \rightarrow b \rightarrow \mathit{Stream}\,a \\ \mathit{unfold}\,f\,b = a : \mathit{unfold}\,f\,b' \qquad\mathbf{where}\qquad (a,b') = f\,b \end{array}$

${\mathit{unfold}\,f}$ generates a stream from a seed, using the body ${f}$ that transforms a seed ${b}$ into an element ${a}$ and a new seed ${b'}$. For example, the map function for streams uses the input stream as the seed, repeatedly splitting it into its head and tail:

$\displaystyle \begin{array}{l} \mathit{mapS} :: (a \rightarrow b) \rightarrow \mathit{Stream}\,a \rightarrow \mathit{Stream}\,b \\ \mathit{mapS}\,f = \mathit{unfold}\,(\mathit{fork}\,(f \cdot \mathit{head}, \mathit{tail})) \end{array}$

where ${\mathit{fork}}$ applies two functions to the same argument:

$\displaystyle \mathit{fork}\,(f,g)\,a = (f\,a, g\,a)$

The crucial property of ${\mathit{unfold}}$ is its universal property, which provides necessary and sufficient conditions for a computation to be expressible as an instance of ${\mathit{unfold}}$:

$\displaystyle h = \mathit{unfold}\,f \Leftrightarrow \mathit{out} \cdot h = \mathit{prod}\,(\mathit{id},h) \cdot f$

where ${\mathit{out} = \mathit{fork}\,(\mathit{head},tail)}$ deconstructs a stream into its head and tail, and

$\displaystyle \mathit{prod}\,(f,g)\,(a,b) = (f\,a, g\,b)$

From the universal property, one can easily (exercise!) prove three simple consequences (we’ll call them the “identity” and two “evaluation” rules):

$\displaystyle \begin{array}{l} \mathit{unfold}\,\mathit{out} = \mathit{id} \\ \mathit{head} \cdot \mathit{unfold}\,(\mathit{fork}\,(f,g)) = f \\ \mathit{tail} \cdot \mathit{unfold}\,(\mathit{fork}\,(f,g)) = \mathit{unfold}\,(\mathit{fork}\,(f,g)) \cdot g \end{array}$

and the very important fusion law:

$\displaystyle \mathit{unfold}\,f \cdot h = \mathit{unfold}\,g \Leftarrow f \cdot h = \mathit{prod}\,(\mathit{id},h) \cdot g$

allowing a preceding function ${h}$ to be absorbed into the unfold.

Making streams a monad amounts to defining functions

$\displaystyle \begin{array}{lcl} \mathit{return} &::& a \rightarrow \mathit{Stream}\,a \\ \mathit{join} &::& \mathit{Stream}\,(\mathit{Stream}\,a) \rightarrow \mathit{Stream}\,a \end{array}$

$\displaystyle \begin{array}{lcl} \mathit{join} \cdot \mathit{return} &=& \mathit{id} \\ \mathit{join} \cdot \mathit{mapS}\,\mathit{return} &=& \mathit{id} \\ \mathit{join} \cdot \mathit{mapS}\,\mathit{join} &=& \mathit{join} \cdot \mathit{join} \end{array}$

Looking at the type, the obvious (indeed, I think the only possible) definition one can give for ${\mathit{return}}$ is ${\mathit{return} = \mathit{repeat}}$ where

$\displaystyle \mathit{repeat} = \mathit{unfold}\,\mathit{double}$

and ${\mathit{double} = \mathit{fork}\,(\mathit{id},\mathit{id})}$ makes two copies of its argument. However, there are many type-correct definitions one could give for ${ \mathit{join}}$, including ${\mathit{head}}$, ${\mathit{mapS}\,\mathit{head}}$, and ${\mathit{diag}}$, where

$\displaystyle \mathit{diag} = \mathit{unfold}\,\mathit{hhtt}$

and where (for brevity in what follows) we define

$\displaystyle \begin{array}{lcl} \mathit{hhtt} &=& \mathit{fork}\,(\mathit{hh},\mathit{tt}) \\ \mathit{hh} &=& \mathit{head}\cdot\mathit{head} \\ \mathit{tt} &=& \mathit{tail}\cdot\mathit{mapS}\,\mathit{tail} \end{array}$

Obviously, ${\mathit{head}}$ yields the first “row” of a stream of streams (if one considers it in row-major order), and ${\mathit{mapS}\,\mathit{head}}$ yields the first column; as the name suggests, ${\mathit{diag}}$ yields the leading diagonal. Nick’s post demonstrates that the first two, although type-correct, do not satisfy the monad laws. He also provides a proof that the third does, which we turn to next.

The proofs that ${\mathit{repeat}}$ and ${\mathit{diag}}$ satisfy the three monad laws are very straightforward, using the universal property of ${\mathit{unfold}}$ and its consequences.

For the first monad law, fusion gives us the condition to check:

$\displaystyle \begin{array}{ll} & \mathit{diag}\cdot\mathit{repeat} = \mathit{id} \\ \Leftarrow & \\ & \mathit{hhtt}\cdot\mathit{repeat} = \mathit{prod}\,(\mathit{id},\mathit{repeat})\cdot\mathit{fork}\,(\mathit{head},\mathit{tail}) \end{array}$

Working on the right-hand side, we have:

$\displaystyle \begin{array}{ll} & \mathit{hhtt}\cdot\mathit{repeat} \\ = & \qquad \{ \mbox{definition} \} \\ & \mathit{fork}\,(\mathit{hh},\mathit{tt})\cdot\mathit{repeat} \\ = & \qquad \{ \mbox{composition distributes backwards over fork} \} \\ & \mathit{fork}\,(\mathit{hh}\cdot\mathit{repeat},\mathit{tt}\cdot\mathit{repeat}) \\ = & \qquad \{ \mbox{definitions} \} \\ & \mathit{fork}\,(\mathit{head}\cdot\mathit{head}\cdot\mathit{repeat},\mathit{tail}\cdot\mathit{mapS}\,\mathit{tail}\cdot\mathit{repeat}) \\ = & \qquad \{ \mbox{evaluation for~} \mathit{repeat} \} \\ & \mathit{fork}\,(\mathit{head},\mathit{tail}\cdot\mathit{mapS}\,\mathit{tail}\cdot\mathit{repeat}) \\ = & \qquad \{ \mbox{naturality; evaluation} \} \\ & \mathit{fork}\,(\mathit{head},\mathit{repeat}\cdot\mathit{tail}) \\ = & \qquad \{ \mbox{pairs} \} \\ & \mathit{prod}\,(\mathit{id},\mathit{repeat}) \cdot \mathit{fork}\,(\mathit{head},\mathit{tail}) \end{array}$

discharging the proof obligation.

Similarly, for the second monad law, fusion gives us the condition:

$\displaystyle \begin{array}{ll} & \mathit{diag}\cdot\mathit{mapS}\,\mathit{repeat} = \mathit{id} \\ \Leftarrow & \\ & \mathit{hhtt}\cdot\mathit{mapS}\,\mathit{repeat} = \mathit{prod}\,(\mathit{id},\mathit{mapS}\,\mathit{repeat})\cdot\mathit{fork}\,(\mathit{head},\mathit{tail}) \end{array}$

and working on the right-hand side, in almost exactly the same steps we get:

$\displaystyle \begin{array}{ll} & \mathit{hhtt}\cdot\mathit{mapS}\,\mathit{repeat} \\ = & \qquad \{ \mbox{definition} \} \\ & \mathit{fork}\,(\mathit{hh},\mathit{tt})\cdot\mathit{mapS}\,\mathit{repeat} \\ = & \qquad \{ \mbox{composition distributes backwards over fork} \} \\ & \mathit{fork}\,(\mathit{hh}\cdot\mathit{mapS}\,\mathit{repeat},\mathit{tt}\cdot\mathit{mapS}\,\mathit{repeat}) \\ = & \qquad \{ \mbox{definitions} \} \\ & \mathit{fork}\,(\mathit{head}\cdot\mathit{head}\cdot\mathit{mapS}\,\mathit{repeat},\mathit{tail}\cdot\mathit{mapS}\,\mathit{tail}\cdot\mathit{mapS}\,\mathit{repeat}) \\ = & \qquad \{ \mbox{naturality; evaluation} \} \\ & \mathit{fork}\,(\mathit{head},\mathit{tail}\cdot\mathit{mapS}\,\mathit{tail}\cdot\mathit{mapS}\,\mathit{repeat}) \\ = & \qquad \{ \mbox{naturality; functors; evaluation} \} \\ & \mathit{fork}\,(\mathit{head},\mathit{mapS}\,\mathit{repeat}\cdot\mathit{tail}) \\ = & \qquad \{ \mbox{pairs} \} \\ & \mathit{prod}\,(\mathit{id},\mathit{mapS}\,\mathit{repeat}) \cdot \mathit{fork}\,(\mathit{head},\mathit{tail}) \end{array}$

discharging the obligation.

What about the third monad law? To apply the universal property (or fusion), we need one side to be expressed as an unfold; but neither side of the equation ${\mathit{diag}\cdot\mathit{diag} = \mathit{diag}\cdot\mathit{mapS}\,\mathit{diag}}$ is in that form. No matter; let us hypothesize that one side—say, the left—can be expressed in the form ${\mathit{unfold}\,h}$ for some ${h}$, then calculate a suitable definition for ${h}$ (if one exists). Assuming we succeed, then we can use fusion to check that the other side equals ${\mathit{unfold}\,h}$. (This strategy doesn’t work if we can find no such ${h}$!)

Again, fusion gives us

$\displaystyle \mathit{diag}\cdot\mathit{diag} = \mathit{unfold}\,h \Leftarrow \mathit{hhtt}\cdot\mathit{diag} = \mathit{prod}\,(\mathit{id},\mathit{diag})\cdot h$

so we calculate:

$\displaystyle \begin{array}{ll} & \mathit{hhtt}\cdot\mathit{diag} \\ = & \qquad \{ \mbox{definition; distribution} \} \\ & \mathit{fork}\,(\mathit{head}\cdot\mathit{head}\cdot\mathit{diag},\mathit{tail}\cdot\mathit{mapS}\,\mathit{tail}\cdot\mathit{diag}) \\ = & \qquad \{ \mbox{evaluation for~} \mathit{diag} \} \\ & \mathit{fork}\,(\mathit{head}\cdot\mathit{head}\cdot\mathit{head},\mathit{tail}\cdot\mathit{mapS}\,\mathit{tail}\cdot\mathit{diag}) \\ = & \qquad \{ \mbox{naturality; evaluation} \} \\ & \mathit{fork}\,(\mathit{head}\cdot\mathit{head}\cdot\mathit{head},\mathit{diag}\cdot\mathit{tail}\cdot\mathit{mapS}\,\mathit{tail}\cdot\mathit{mapS}\,(\mathit{mapS}\,\mathit{tail})) \\ = & \qquad \{ \mbox{pairs} \} \\ & \mathit{prod}\,(\mathit{id},\mathit{diag})\cdot\mathit{fork}\,(\mathit{head}\cdot\mathit{head}\cdot\mathit{head},\mathit{tail}\cdot\mathit{mapS}\,\mathit{tail}\cdot\mathit{mapS}\,(\mathit{mapS}\,\mathit{tail})) \end{array}$

Therefore, letting

$\displaystyle \mathit{hhhttt} = \mathit{fork}\,(\mathit{head}\cdot\mathit{head}\cdot\mathit{head},\mathit{tail}\cdot\mathit{mapS}\,\mathit{tail}\cdot\mathit{mapS}\,(\mathit{mapS}\,\mathit{tail}))$

we have concluded that

$\displaystyle \mathit{diag}\cdot\mathit{diag} = \mathit{unfold}\,\mathit{hhhttt}$

Now all we have to do is to check that the right-hand side of the third monad law also equals this; fusion gives us the condition

$\displaystyle \begin{array}{ll} & \mathit{diag}\cdot\mathit{mapS}\,\mathit{diag} = \mathit{unfold}\,\mathit{hhhttt} \\ \Leftarrow & \\ & \mathit{hhtt}\cdot\mathit{mapS}\,\mathit{diag} = \mathit{prod}\,(\mathit{id},\mathit{mapS}\,\mathit{diag})\cdot \mathit{hhhttt} \end{array}$

and we calculate on the right-hand side:

$\displaystyle \begin{array}{ll} & \mathit{hhtt}\cdot\mathit{mapS}\,\mathit{diag} \\ = & \qquad \{ \mbox{definition; distribution} \} \\ & \mathit{fork}\,(\mathit{head}\cdot\mathit{head}\cdot\mathit{mapS}\,\mathit{diag},\mathit{tail}\cdot\mathit{mapS}\,\mathit{tail}\cdot\mathit{mapS}\,\mathit{diag}) \\ = & \qquad \{ \mbox{naturality; evaluation} \} \\ & \mathit{fork}\,(\mathit{head}\cdot\mathit{head}\cdot\mathit{head},\mathit{tail}\cdot\mathit{mapS}\,\mathit{tail}\cdot\mathit{mapS}\,\mathit{diag}) \\ = & \qquad \{ \mbox{functors; naturality; evaluation} \} \\ & \mathit{fork}\,(\mathit{head}\cdot\mathit{head}\cdot\mathit{head},\mathit{mapS}\,\mathit{diag}\cdot\mathit{tail}\cdot\mathit{mapS}\,\mathit{tail}\cdot\mathit{mapS}\,(\mathit{mapS}\,\mathit{tail})) \\ = & \qquad \{ \mbox{pairs; definition} \} \\ & \mathit{prod}\,(\mathit{id},\mathit{mapS}\,\mathit{diag})\cdot\mathit{hhhttt} \end{array}$

completing the proof.

As you’ll see, the calculations are all quite short and simple, whereas in Nick’s formulation, they were rather hard work; I think that was (a) because he wasn’t exploiting the universal property, and (b) because he was working in terms of the “bind” rather than the “join” of the monad, which forced him into a more pointwise rather than pointfree style. Points are helpful when writing programs, but less so when reasoning about them.

## Deducing diag

Here’s another way of looking at the problem. Nick’s blog presented three plausible (that is, type-correct) definitions for the ${\mathit{join}}$ operation. Two of these didn’t satisfy the necessary laws, so were evidently wrong. The third, ${\mathit{diag}}$, does satisfy the laws, but is it the only possible definition that does? I believe that it is the only solution in the form of an unfold; but I only have a hand-waving argument as to why.

Let us suppose that indeed

$\displaystyle join = \mathit{unfold}\,k$

for some ${k}$. Without loss of generality, let us suppose also that

$\displaystyle k = \mathit{fork}\,(k_1,k_2)$

with

$\displaystyle \begin{array}{lcl} k_1 &::& \mathit{Stream}\,(\mathit{Stream}\,a) \rightarrow a \\ k_2 &::& \mathit{Stream}\,(\mathit{Stream}\,a) \rightarrow \mathit{Stream}\,(\mathit{Stream}\,a) \end{array}$

I claimed above that ${\mathit{repeat}}$ is the only type-correct definition of the ${\mathit{return}}$ operation. (Ignoring bottoms, that is. Which is to say, in Haskell, all type-correct definitions are approximations in the definedness ordering to ${\mathit{repeat}}$.)

Consideration of just the first two monad laws gives us some constraints on ${k}$, since we know that ${\mathit{return} = \mathit{repeat}}$:

$\displaystyle \begin{array}{lcl} k\cdot\mathit{repeat} &=& \mathit{prod}\,(\mathit{id},\mathit{repeat})\cdot\mathit{fork}\,(\mathit{head},\mathit{tail}) \\ k\cdot\mathit{mapS}\,\mathit{repeat} &=& \mathit{prod}\,(\mathit{id},\mathit{mapS}\,\mathit{repeat})\cdot\mathit{fork}\,(\mathit{head},\mathit{tail}) \end{array}$

Or in terms of ${k}$‘s two components,

$\displaystyle \begin{array}{lcll} k_1\cdot\mathit{repeat} &=& \mathit{head} &(1)\\ k_2\cdot\mathit{repeat} &=& \mathit{repeat}\cdot\mathit{tail} &(2)\\ k_1\cdot\mathit{mapS}\,\mathit{repeat} &=& \mathit{head} &(3)\\ k_2\cdot\mathit{mapS}\,\mathit{repeat} &=& \mathit{mapS}\,\mathit{repeat}\cdot\mathit{tail} &(4) \end{array}$

I claim that (1) entails that ${k_1}$ picks some element out of the first “column” of a stream of streams (thinking of the input as an infinite matrix in row-major order again)—for the equation says that when the input consists of infinitely many copies of the same stream, ${k_1}$ picks (one of the many copies of) the head of that stream. Symmetrically, (3) entails that, when given a infinite matrix whose columns are all equal, ${k_1}$ picks some element out of the first “row”. And because ${k_1}$ has to be polymorphic, it cannot behave differently on special matrices like these than it does in general. Putting those statements together, and waving my hands in the air, I conclude that ${k_1}$ picks the only element that is in both the first row and the first column:

$\displaystyle k_1 = \mathit{head} \cdot \mathit{head}$

Similarly, Equation (2) says that, given an infinite input matrix all of whose rows are equal, ${k_2}$ drops the first column (and possibly some of the rows are duplicated or dropped, and the order of the rows may change; but the elements of the rows are untouched). Symmetrically, (4) says that, given an input whose columns are all equal, ${k_2}$ drops the first row (and may duplicate, drop, or rearrange the columns, but not change any of them). And again, the behaviour in general must be consistent with these special cases. Putting these observations together, ${k_2}$ must drop the first row and the first column, and cannot change any of the remainder of the matrix.

$\displaystyle k_2 = \mathit{tail} \cdot \mathit{mapS}\,\mathit{tail}$

What is the right framework in which to present such arguments more formally? It feels rather like Paul Hoogendijk’s relational approach to generic programming, which has to talk about largest natural transformations of a given type: the relational setting provides the conjunction one needs in order to express the two separate constraints on ${k_1}$.

Posted in Uncategorized | 11 Comments

## Design patterns as higher-order datatype-generic programs

Well, I got side-tracked from working directly on the book. One of the sidetracks was working on my paper Design Patterns as Higher-Order Datatype-Generic Programs from the Workshop on Generic Programming in 2006, revising and extending it for a journal; I’ve put the revised version online. In my defence, I offer that although this isn’t directly content for the book, it is indirectly so.

The central argument of the paper is that current mainstream programming languages such as Java and C# are not expressive enough to allow one to capture the code parts of design patterns such as the Visitor pattern. However, functional languages such as Haskell are sufficiently expressive—which I demonstrate in the paper by providing Haskell representations of four of the GOF patterns.

As the title of the paper suggests, the specific concepts that Haskell provides but current mainstream languages do not are higher-order (parametrization by a function, sometimes called a “lambda” or a “closure”) and datatype-generic (parametrization by a type functor) features. I’ve taken to calling programs exploiting these features “HODGPs”, and languages providing them as “HODGP languages”. A HODGP language lets you capture the code of design patterns as highly flexible reusable software components. Interestingly, Scala also provides HODGP features, together with everything you’d expect from an OO language; I’m hopeful that Java and C# will follow Scala’s lead (or that Scala will supercede them!). Bruno Oliveira‘s DPhil thesis Genericity, Extensibility and Type-Safety in the Visitor Pattern explored using Scala for HODGPs.

Of course, I admit that “capturing the code parts of a pattern” is not the same as capturing the pattern itself. There is more to the pattern than just the code; the “prose, pictures, and prototypes” form an important part of the story, and are not captured in a HODGP representation of the pattern. So the HODGP isn’t a replacement for the pattern.

The four GOF patterns I discuss in the paper are Composite, Iterator, Visitor and Builder. My claim is that Composite (hierarchical structures) amounts to recursive datatypes, Iterator (linear traversals over the elements of a collection) to maps, Visitor (structured traversals also exploiting the shape of a collection) to folds, and Builder (separating the construction of an object from its representation) to unfolds and builds. This is a simplification, both of the patterns and the paper; take a read if you want the full story!

Posted in Uncategorized | 6 Comments

## The story so far

I’ve already written a fair amount on these topics, and I don’t propose to blog that as I go. If you’d like some background, you might want to look at the following notes of mine:

Of course, many others have also written on these topics too. Some articles that have particularly inspired me are:

(I’m sure there are many others too, which I’ve forgotten to mention.)

Posted in Uncategorized | 3 Comments

## Recursion patterns

The central idea in this book is the importance of recursion patterns in functional programming. One of the simplest examples is the map operator on lists, defined in Haskell as follows:

$\begin{array}{lcl} \mathit{map}\;f\;[\,] &=& [\,] \\ \mathit{map}\;f\;(x:xs) &=& f\;x : \mathit{map}\;f\;xs \end{array}$

(Intuitively, $\mathit{map}$ applies a function $f$ to every element of a list, returning a new list. When $\mathit{map}\;f$ is applied to the empty list $[\,]$, it returns the empty list; applied to a non-empty list $x:xs$ with head $x$ and tail $xs$, it returns the list whose head is $f$ applied to $x$, and whose tail is $\mathit{map}\;f$ applied recursively to $xs$. Because the function $\mathit{map}$ accepts another function $f$ as an argument, it is called a higher-order function.)

Another example familiar to Haskell programmers is the fold operator on lists:

$\begin{array}{lcl} \mathit{foldr}\;f\;e\;[\,] &=& e \\ \mathit{foldr}\;f\;e\;(x:xs) &=& f\;x\;(\mathit{foldr}\;f\;e\;xs) \end{array}$

(Intuitively, this “folds” a list up into a value; the empty list is folded into the initial value $e$, and a non-empty list is folded by recursively folding the tail then combining the result of this with the head using the binary function $f$.)

One can think of the operators $\mathit{map}$ and $\mathit{foldr}$ as abstracted patterns of computation: many useful functions can be expressed in terms of them, and identifying them as useful and reusable concepts saves a lot of repetition in code. Put another way, functional programming (especially lazy functional programming) languages provide the programmer with good tools for building their own control structures; if you don’t have the right kind of loop built-in, just define it as a higher-order function.

But there’s another benefit to be derived from certain recursion patterns (in particular, for the map and fold above, but not for any old custom control structure that you might just have defined). Take the definition of $\mathit{foldr}$, but abstract from the $\mathit{foldr}\;f\;e$ part:

$\begin{array}{lcl} h\;[\,] &=& e \\ h\;(x:xs) &=& f\;x\;(h\;xs) \end{array}$

and read this as an equation in the unknown $h$, for fixed $f$ and $e$. It turns out that this equation has a unique solution (modulo some subtleties, as we’ll cover later) — which is, as you might have guessed, $h = \mathit{foldr}\;f\;e$. This is called the universal property of $\mathit{foldr}$, and it is very convenient for reasoning about programs with. For example, to show that some complicated expression equals a given fold, it suffices to show that the expression satisfies the universal property for that fold. Such universal properties will come up again and again throughout the book.

Posted in Uncategorized | 1 Comment

## Functional programming

So, what is the “functional programming” in the title about, then? Here’s a very brief characterization, for those who haven’t heard of it before. I’m mostly thinking of the Haskell programming language, and there’s a good explanation and many resources at www.haskell.org.

In a nutshell, functional programming restricts itself to programming with values, rather than with actions. Most programming languages are “imperative”, focussing on the actions: the program describes a series of actions to perform, and only makes incidental use of values in passing; there is a sublanguage of statements (such as assignments to variables, loops, conditional choices) and a sublanguage of expressions (such as for the computation yielding the value to be assigned to a variable in an assignment statement, and for the condition on which a conditional depends).

In contrast, pure functional programming languages dispense with the statements, and make use only of expressions. This might seem very limiting, restricting programs to variations on a mere pocket calculator. But of course, a useful functional language extends the grammar of expressions, so that they cover much more than arithmetic; indeed, expressions typically encompass complex data structures and recursive function definitions, and so are every bit as expressive as statements. Moreover, it turns out that programs expressed in terms of expressions rather than statements are usually shorter (many of the details of the equivalent imperative program are redundant) and simpler (because there are no assignment statements, variables don’t vary, and so the familiar equational reasoning principles of high-school algebra are applicable throughout).

The characterization of programming languages as “functional” versus “imperative” is by no means exhaustive; there are many other styles too. But many of them are also discovering the joys of functional programming; for example, good practice in object-oriented programming states that value objects should be immutable.

Posted in Uncategorized | 1 Comment