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).
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).
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 :
generates a stream from a seed, using the body that transforms a seed into an element and a new seed . For example, the map function for streams uses the input stream as the seed, repeatedly splitting it into its head and tail:
where applies two functions to the same argument:
The crucial property of is its universal property, which provides necessary and sufficient conditions for a computation to be expressible as an instance of :
where deconstructs a stream into its head and tail, and
From the universal property, one can easily (exercise!) prove three simple consequences (we’ll call them the “identity” and two “evaluation” rules):
and the very important fusion law:
allowing a preceding function to be absorbed into the unfold.
Streams as a monad
Making streams a monad amounts to defining functions
satisfying the monad laws:
Looking at the type, the obvious (indeed, I think the only possible) definition one can give for is where
and makes two copies of its argument. However, there are many type-correct definitions one could give for , including , , and , where
and where (for brevity in what follows) we define
Obviously, yields the first “row” of a stream of streams (if one considers it in row-major order), and yields the first column; as the name suggests, 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.
Checking the monad laws
The proofs that and satisfy the three monad laws are very straightforward, using the universal property of and its consequences.
For the first monad law, fusion gives us the condition to check:
Working on the right-hand side, we have:
discharging the proof obligation.
Similarly, for the second monad law, fusion gives us the condition:
and working on the right-hand side, in almost exactly the same steps we get:
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 is in that form. No matter; let us hypothesize that one side—say, the left—can be expressed in the form for some , then calculate a suitable definition for (if one exists). Assuming we succeed, then we can use fusion to check that the other side equals . (This strategy doesn’t work if we can find no such !)
Again, fusion gives us
so we calculate:
we have concluded that
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
and we calculate on the right-hand side:
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.
Here’s another way of looking at the problem. Nick’s blog presented three plausible (that is, type-correct) definitions for the operation. Two of these didn’t satisfy the necessary laws, so were evidently wrong. The third, , 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
for some . Without loss of generality, let us suppose also that
I claimed above that is the only type-correct definition of the operation. (Ignoring bottoms, that is. Which is to say, in Haskell, all type-correct definitions are approximations in the definedness ordering to .)
Consideration of just the first two monad laws gives us some constraints on , since we know that :
Or in terms of ‘s two components,
I claim that (1) entails that 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, 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, picks some element out of the first “row”. And because 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 picks the only element that is in both the first row and the first column:
Similarly, Equation (2) says that, given an infinite input matrix all of whose rows are equal, 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, 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, must drop the first row and the first column, and cannot change any of the remainder of the matrix.
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 .