A while back Brent Yorgey http://byorgey.wordpress.com posted a menagerie of types. A very nice survey of types in Haskell, including, among other things, the monadic types.
A reader posted a question, framed with 'you know, it'd be a lot easier for me to understand monads if you provided an implementation in Java.'[1]
Well, that reader really shouldn't have done that.
Really.
Because it got me to thinking, and dangerous things comes out of geophf's thoughts ... like monads in Java.
Let's do this.
Problem Statement
Of course, you just don't write monads for Java. You need some motivation. What's my motivation?
Well, I kept running up against the Null Object pattern, because I kept running up against null in the Java runtime, because there's a whole lot of optionality in the data sets I'm dealing with, and instead of using the Null Object, null is used to represent absence.
Good choice?
Well, it's expedient, and that's about the best I can say for that.
So I had to keep writing the Null Object pattern for each of these optional element types I encountered.
I encounter quite a few of them ... 2,100 of them and counting.
So I generalized the Null object pattern using generic types, and that worked fine ...
But I kept looking at the pattern. The generalization of the Null Object pattern is Nothing, and a present instance is Just that something.
I had implemented non-monadic Maybe.
And the problem with that is that none of the power of Maybe, as a Monad, is available to a generalized Null Object pattern.
Put another way: I wish to do something given that something is present.
Put another-another way: bind.
So, after a long hard look ('do I really want to implement monads? Can't I just settle for 'good enough' ... that really isn't good enough?), I buckled down to do the work of implementing not just Maybe (heh: 'Just Maybe'), but Monad itself.
Did it pay off? Yes, but wait and see. First the implementation. But even before that, let's review what a monad is.
What the Hell is a Monad?
Everybody seems to ask this question when first encountering monads, and everybody seems to come up with their own explanations, so we have tutorials that explain Monads as things as far-ranging from spacesuits to burritos.
My own explanation is to punt ... to category theory.
A monad is simply a triple (that's why it's called a monad, ... because it's a triple), defined thusly:
(T, η, μ)
Simple right?
Don't leave me!
Okay, yes. I understand you are rolling your eyes and saying 'well, that's all Greek to me.'
So allow me to explain in plain language the monad.
Monad is the triple (T, η, μ) where
T is the Monad Functorη is the unit function that lifts an ordinary object (a unit) into the Monad functor; and,μ is the join function that takes a composed monad M (M a) and returns the simplified type of the composition, or M a.
And that is (simply) what the hell a Monad is. What a monad can do ... well, there are articles galore about that, and, later, I will provide examples of what Monad gives us ... in Java, no less.
The Implementation
We need to work our way up to Monad. There's a whole framework, a way of thinking, a context, that needs to be in place for Monad to be effective or even to exist. Monad is 'happy' in the functional world, so we need to implement functions.
Or more correctly, 'functionals' ... in Haskell, they are called 'Functors.'
A functor is a container, and the function of functors is to take an ordinary function, which we write: f: a → b (pronounced "the function f from (type) a to (type) b" and means that f takes an argument of type a and returns a result of type b), and give a function g: Functor a → Functor b.
Functor basically is a container for the function fmap: Functor f ⇒ (a → b) → (f a → f b)
Well, is Functor the fundamental type? Well, yes and no.
It is, given that we have functions defined. In Java, we don't have that. We have methods, yes, but we don't have free-standing functions. Let's amend that issue:
<jcode>
<jkey>public interface</jkey> Applicable<T1, T2> {
<jkey>public</jkey> T2 apply(T1 arg) <jkey>throws</jkey> Failure;
};</jcode>
And what's this Failure thingie? It's simply a functional exception, so:
<jcode>
<jkey>public class</jkey> Failure <jkey>extends</jkey> Exception {
<jkey>public</jkey> Failure(String string) {
<jkey>super</jkey>(string);
}
/// and the serialVersionUID for serialization; your IDE can define that
}</jcode>
I call a Function 'Applicable' because in functional languages that's what you do: apply a function on (type) a to get (type) b. And, using Java Generics terminology, type a is T1 and type b is T2. So we're using pure Java to write pure Java code and none will be the wiser that we're actually doing Category Theory via a Haskell implementation ... in Java, right?
Right.
So, now we have functions (Applicable), we can provide the declaration of the Functor type:
<jcode>
<jkey>public interface</jkey> Functor<F, T> {
<jkey>public</jkey> <T1> Applicable<? <jkey>extends</jkey> Functor<F, T>,
? <jkey>extends</jkey> Functor<F, T1>>
fmap(Applicable<T, T1> f) <jkey>throws</jkey> Failure;
<jkey>public</jkey> T arg() <jkey>throws</jkey> Failure;
}</jcode>
The above definition of fmap is the same declaration (in Java) as its functional declaration: it takes a function f: a → b and gives a function g: Functor a → Functor b
Okay, we're half-way there. A Monad is a Functor, and we have Functor declared.
The unit function, η, comes for free in Java: it's called new.
So that leaves the join function μ.
And defining join for a specific monad is simple. Join for the list monad is append. Join for the Maybe monad and the ID monad is arg. What about join for just Monad?
Well, there is no definition of such, but we can declare its type:
<jcode>
<jkey>public interface</jkey> Joinable<F, T> <jkey>extends</jkey> Functor<F, T> {
<jkey>public</jkey> Functor<F, ?> join() <jkey>throws</jkey> Failure;
}</jcode>
Too easy! you complain.
Well, isn't it supposed to be? Join is simply a function that takes a functor and returns functor.
The trick is that we have to ensure that T is of type Functor<F, ?>, and we leave that an implementation detail for each specific monad implementing join.
That was easy!™
Monad
So now that we have all the above, Functor, Join, and Unit, we have Monad:
... BUT WAIT!
And here's the interlude of where the power of Monad comes in: bind.
What is bind? Bind is a function that says: do something in the monadic domain.
Really, that sounds boring, right? But it's a very powerful thing. Because once we are in the monadic domain, we can guarantee things that we cannot in Java category (if there is such).
(There is. I just declared it.)[2]
So, in the monadic domain, a function thus bound can be guaranteed to, e.g., be working with an instance and not a null.
Guaranteed.
AND! ...
Well, what is bind?
Bind is a function that takes an ordinary value and returns a result in the monadic domain:
Monad m ⇒ bind: a → m b
So the 'AND!' of this is that bind can be chained ... meaning we can go from guarantee to guarantee, threading a safe computation from start to finish.
Monad gives us bind.
And the beauty of Monad? bind comes for free, for once join is defined, bind can be defined in terms of join:
Monad m ⇒ bind (f: a → m b) (m a) = join ((fmap f) (m a))
Do you see what is happening here? We are using fmap to lift the function f one step higher into the monadic domain, so fmap f gives the function Monad m ⇒ g: m a → m (m b) so we are not actually passing in a value of type a, we are passing in the Monad m a, and then we get back a type of m (m b) which then join does it magic to simplify to the monadic type m b.
So to the outside world, it looks like we are passing in an a to get an m b but this definition allows monadic chaining, for a becomes m a and then m (m b) is simplified to m b that — and here's the kicker — is passed to the next monadically bound function.
You can chain this as far as you'd like:
m a >>= f >>= g >>= ... >>= h → m z
And since the computation occurs in the monadic domain, you are guaranteed the promise of that domain.
There is the power of monadic programming.
Given that explanation, and remembering that bind can be defined in terms of join, let's define Monad:
<jcode>
<jkey>public abstract class</jkey> Monad<M, A> <jkey>implements</jkey> Joinable<M, A> {
<jkey>public</jkey> <T> Monad<M, T> bind(Applicable<A, Monad<M, T>> f) <jkey>throws</jkey> Failure {
Applicable<Monad<M, A>, Monad<M, Monad<M, T>>> a
= (Applicable<Monad<M, A> Monad<M, Monad<M, T>>>) fmap(f);
Monad<M, Monad<M, T>> mmonad = a.apply(<jkey>this</jkey>);
<jkey>return</jkey> (Monad<M, T>) mmonad.join();
}
<jkey>public</jkey> Monad<M, A> fail(String ex) <jkey>throws</jkey> Failure {
<jkey>throw new</jkey> Failure(ex);
}
}</jcode>
The bind implementation is exactly as previously discussed: bind is the application of the fmap of f with the joined result returned. So, we simply define join for subclasses, usually a trivial definition, and we have the power of bind automagically!
Now fail is an interesting beast in subclasses, because in the monadic domain, failure is not always a bad thing, or even an exceptional one, and can be quite, and very, useful. Some examples, fail represents 'zero' in the monadic domain, so 'failure' for list is the empty list, and 'failure' for Maybe is Nothing. So, when failure occurs, the computation can continue gracefully and not always automatically abort from the computation, which happens with the try/catch paradigm.
There you have it: Monads in Java!
The rest of the story: ... Maybe
So, we could've ended this article right now, and you have everything you need to do monadic programming in Java. But so what? A programming paradigm isn't useful if there are no practical applications. So let's give you one: Maybe.
Maybe is a binary type, it is either Nothing or Just x where x is whatever value that is what we're really looking for (as opposed to the usual case in Java: <jkey>null</jkey>).
So, let's define the Maybe type in Java.
First is the protocol that extends the Monad:
<jcode>
<jkey>public abstract class</jkey> Maybe<A> <jkey>extends</jkey> Monad<Maybe, A> {
</jcode>
Do you see how the Maybe type declares itself as a Monad in its own definition? I just love that.
Anyway.
As mentioned before, fail for Maybe is Nothing:
<jcode>
<jkey>public</jkey> Maybe<A> fail(String ex) <jkey>throws</jkey> Failure {
<jkey>return</jkey> (Maybe<A>) NOTHING;
}</jcode>
(NOTHING is a constant in Maybe to be defined later. Before we define it ('it' being NOTHING), recall that a Monad is a Functor so we have to define fmap. Let's do that now)
<jcode>
<jkey>protected abstract</jkey> <T> Maybe<T>
mbBind(Applicable<A, Monad<Maybe, T>> arg) <jkey>throws</jkey> Failure;
<jkey>public</jkey> <T> Applicable<Maybe<A>, Maybe<T>>
fmap(<jkey>final</jkey> Applicable<A, T> f) <jkey>throws</jkey> Failure {
<jkey>return new</jkey> Applicable<Maybe<A>, Maybe<T>>() {
<jkey>public</jkey> Maybe<T> apply(Maybe<A> arg) <jkey>throws</jkey> Failure {
Applicable<A, Monad<Maybe, T>> liFted =
<jkey>new</jkey> Applicable<A, Monad<Maybe, T>>() {
<jkey>public</jkey> Maybe<T> apply(A arg) <jkey>throws</jkey> Failure {
<jkey>return</jkey> Maybe.pure(f.apply(arg));
}
};
<jkey>return</jkey> (Maybe<T>)arg.mbBind(liFted);
}
};
}</jcode>
No surprises here. fmap lifts the function f: a → b to Maybe m ⇒ g: m a → m b where in this case the Functor is a Monad, and this case, that Monad is Maybe.[3]
There is the small issue(s) of what the <jkey>static</jkey> method pure and the method mbBind are, but these depend on the definitions of the subclasses NOTHING and Just, so let's define them now.
<jcode>
<jkey>public static final</jkey> Maybe<?> NOTHING = <jkey>new</jkey> Maybe() {
<jkey>public</jkey> String toString() {
<jkey>return</jkey> "Nothing";
}
<jkey>public</jkey> Object arg() <jkey>throws</jkey> Failure {
<jkey>throw new</jkey> Failure("Cannot extract a value from Nothing.");
}
<jkey>public</jkey> Functor join() <jkey>throws</jkey> Failure {
<jkey>return this</jkey>;
}
<jkey>protected</jkey> Maybe mbBind(Applicable f) {
<jkey>return this</jkey>;
}
};</jcode>
Trivial definition, as the Null Object pattern is trivial. But do note that the bind operation does not perform the f computation, but skips it, returning Nothing, and forwarding the computation. This is expected behavior, for:
Nothing >>= f → Nothing
The definition of the internal class Just is nearly as simple:
<jcode>
<jkey>public final static class</jkey> Just<J> <jkey>extends</jkey> Maybe<J> {
<jkey>public</jkey> Just(J obj) {
_unit = obj;
}
<jkey>public</jkey> Maybe<?> join() <jkey>throws</jkey> Failure {
<jkey>try</jkey> {
<jkey>return</jkey> (Maybe<?>)_unit;
} <jkey>catch</jkey>(ClassCastException ex) {
<jkey>throw new</jkey> Failure("Joining on a flat structure!");
}
}
<jkey>public</jkey> String toString() {
<jkey>return</jkey> "Just " + _unit;
}
<jkey>public</jkey> Object arg() <jkey>throws</jkey> Failure {
<jkey>return</jkey> _unit;
}
<jkey>protected</jkey> <T> Maybe<T>
mbBind(Applicable<J, Monad<Maybe, T>> f) <jkey>throws</jkey> Failure {
<jkey>return</jkey> (Maybe<T>)f.apply(_unit);
}
<jkey>private final</jkey> J _unit;
}</jcode>
As you can see, the slight variation to NOTHING for Just is that join returns the _unit value if it's the Maybe type (and throws a Failure if it isn't), and mbBind applies the monadic function f to the Just value.
And with the definition of Just we get the <jkey>static</jkey> method pure:
<jcode>
<jkey>public static</jkey> <T> Maybe<T> pure(T x) {
<jkey>return new</jkey> Just<T>(x);
}</jcode>
And then we close out the Maybe implementation with:
<jcode>}</jcode>
Simple.
Practical Example
Maybe is useful for any semideterministic programming, that is: where something may be true, or it may not be. But the question I keep getting, from Java coders, is this: "I have these chains of getter methods in my web interface to my data objects to set a result, but I often have <jkey>null</jkey>s in some values gotten along the chain. How do I set the value from what I've gotten, or do nothing if there's a <jkey>null</jkey> along the way."
"Fine, no problems ..." I begin, but then they interrupt me.
"No, I'm not done yet! I have like tons of these chained statements, and I don't want to abort on the first one that throws a NullPointerException, I just want to pass through the statement with the <jkey>null</jkey> gracefully and continue onto the next assignment. Can your weirdo stuff do that?"
Weirdo stuff? Excusez moi?
I don't feel it's apropos that functionally pure languages have no (mutable) assignment, as that throws provability out the window and is therefore the root of all evil.
No matter how sorely tempted I am.
So, instead I say: "Yeah, that's a bigger problem [soto voce: so you should switch to Haskell!], but the same solution applies."[4]
So, let's go over the problem and a set of solutions.
The problem is something like:
<jcode><jkey>
try</jkey> {
foo.setD(getA().getB().getC().getD());
foo.setE(getA().getB().getC().getE());
bar.setJ(getF().getG().getH().getJ());
bar.setM(getF().getG().getK().getM());
// and ... oh, more than 2000 more assignments ... 'hypothetically'
} <jkey>catch</jkey>(Exception ex) {
ex.printStackTrace();
}</jcode>
And the problem is this: anywhere in any chain of gets, if something goes wrong, the entire computation is stopped from that point, even if there are, oh, let's say, 1000 more valid assignments.
A big, and real, problem. Or 'challenge,' if you prefer.
Now this whole problem would go away if the Null Object pattern was used everywhere. But how to enforce that? In the Java category, you cannot. Even if you make the generic Null Object the base object, the <jkey>null</jkey> is still Java's &bottom — it's 'bottom' — as low as you go in a hierarchy, <jkey>null</jkey> is still an allowable argument everywhere.
And if getA(), or getB(), or getC() return <jkey>null</jkey> you've just failed out of your entire computation with an access attempt to a null pointer.
Solutions
Solution 1: test until you puke
The first solution is to test for null at every turn. And you know what that looks like, but here you go. Because why? Because if you think it or code it, you've got to look at it, or I've got to look at it, so here it is:
<jcode>
A a = getA();
<jkey>if</jkey>(a != <jkey>null</jkey>) {
B b = a.getB();
<jkey>if</jkey>(b != <jkey>null</jkey>) {
C c = b.getC();
<jkey>if</jkey>(c != <jkey>null</jkey>) {
foo.setD(c.getD());
}
}
}</jcode>
What's the problem with this code?
Oh, no problems, just repeat that deep nesting for every single assignment? So you have [oh, let's say 'hypothetically'] 2000 of these deeply nested conditional blocks?
And, besides the fact that it entirely clutters the simple assignment:
<jcode>foo.setD(getA().getB().getC().getD());</jcode>
in decision logic and algorithms that are totally unnecessary and entirely too much clutter.
All I'm doing is assigning a D to a foo! So why do I have to juggle all this conditional code in my head to reach that eventual assignment.
Solution 1 is bunk.
Solution 2: narrow the catch
So, solution 1 is untenable. But we need to assign where we can and skip where we can't. So how about this?
<jcode><jkey>
try</jkey> {
foo.setD(getA().getB().getC().getD());
} <jkey>catch</jkey>(Exception ex) {
// Intentionally empty; silently don't assign if we cannot;
}
<jkey>try</jkey> {
foo.setE(getA().getB().getC().getE());
} <jkey>catch</jkey>(Exception ex) {
// ditto
}
<jkey>try</jkey> {
bar.setJ(getF().getG().getH().getJ());
} <jkey>catch</jkey>(Exception ex) {
// ditto
}
<jkey>try</jkey> {
bar.setM(getF().getG().getK().getM());
} <jkey>catch</jkey>(Exception ex) {
// ditto
}</jcode>
And I say to this solution, meh! Granted, it's much better than solution 1, but, again, you made a computational flow described declaratively in the problem to be these set of staccato statements, having the reader of your code switch into and out of context for every statement.
Wouldn't it be nice to have all the statements together in one block, because, computationally, that's what is happening: a set of data is collected from one place and moved to another, and that is what we wish to describe by keep these assignment grouped in one block.
Solution 3: Maybe Monad
And that's what we can do with monads. It's going to look a bit different that how you're used to the usual Java fair, as we have to lift the statements in the Java category into expressions in the monadic one.
So here goes.
First of all, we need to define generic functions (not methods![5]) for getting values from objects and setting values into object in the monadic domain:
<jcode><jkey>
public abstract class</jkey> SetterM<Receiver, Datum>
<jkey>implements</jkey> Applicable<Datum, Monad<Maybe, Receiver>> {
<jkey>protected</jkey> SetterM(Receiver r) {
<jkey>this</jkey>.receiver = r;
}
// a monadic set function
<jkey>public final</jkey> Monad<Maybe, Receiver> apply(Datum d) <jkey>throws</jkey> Failure {
set(receiver, d);
<jkey>return</jkey> Maybe.pure(receiver);
}
// subclasses implement with the particular set method being called
<jkey>protected abstract void</jkey> set(Receiver r, Datum d);
<jkey>private final</jkey> Receiver receiver;
}</jcode>
This declares a generic setter, so to define setD on the foo instance, we would do the following:
<jcode>
SetterM<Foo, D> setterDinFoo = <jkey>new</jkey> SetterM<Foo, D>(foo) {
<jkey>protected void</jkey> set(Foo f, D d) {
f.setD(d);
}
};</jcode>
The getter functional is similarly defined, with the returned value lifted into (or 'wrapped in,' if you prefer) the Maybe type:
<jcode>
<jkey>public abstract class</jkey> GetterM<Container, Returned>
<jkey>implements</jkey> Applicable<Container, Monad<Maybe, Returned>> {
<jkey>public</jkey> Monad<Maybe, Returned> apply(Container c) <jkey>throws</jkey> Failure {
Maybe<Returned> ans = (Maybe<Returned>)Maybe.NOTHING;
Returned result = get(c);
// c inside the monad is guaranteed to be an instance
// but result has NO guarantees!
<jkey>if</jkey>(result != <jkey>null</jkey>) {
ans = Maybe.pure(result);
// and now ans is inside the monad it must have a value.
// ... even if that value is NOTHING
}
<jkey>return</jkey> ans;
}
<jkey>protected abstract</jkey> Returned get(Container c);
}</jcode>
With the above declaration, a getter monadic function (again, not method) is simply defined:
<jcode>
GetterM<A, B> getterBfromA = <jkey>new</jkey> GetterM<A, B>() {
<jkey>protected B</jkey> get(A a) {
<jkey>return</jkey> a.getB();
}
};</jcode>
In Haskell, the bind operator has a data-flow look to it: (>>=), so writing one of the 'assignments' is as simple as flowing the data to the setter:
getA >>= getB >>= getC >>= getD >>= setD foo
But we have no operator definitions, so we must soldier on using the Java syntax:
<jcode>
<jkey>try</jkey> {
getterA.apply(<jkey>this</jkey>).bind(getterBfromA).bind(getterCfromB).bind(getterDfromC).bind(setterDinFoo);
} <jkey>catch</jkey> {
// a superfluous catch block
}</jcode>
That's one of the assignment expressions.[6]
Let's walk through what happens with a couple of examples.
Let's say that A has a value of a, but B is <jkey>null</jkey>. What happens?
getterA forwards Just a to getterBfromAgetterBfromA gets a <jkey>null</jkey>, converts that into a NOTHING and forwards that to getterCfromBgetterCfromB forwards the NOTHING to getterDfromCgetterDfromC forwards the NOTHING to setterDinFoosetterDinFoo simply returns NOTHING.
And we're done (that is: we're done doing, literally:
NOTHING).
Let's counter with an example where every value has an instance:
getterA forwards Just a to getterBfromAgetterBfromA gets a b, converts that into Just b and forwards that to getterCfromBgetterCfromB gets a c, converts that into Just c and forwards that to getterDfromCgetterDfromC gets a d, converts that into Just d and forwards that to setterDinFoosetterDinFoo gets the wrapped d and sets that value in the Foo instance.
Voilà!
The beauty of this methodology is that we can put them all into one block, and every expression will be evaluated and in a type-safe manner, too, as NOTHING will protect us from a null pointer access:
<jcode>
<jkey>try</jkey> {
getterA.apply(this).bind(getterBfromA).bind(getterCfromB).bind(getterDfromC).bind(setterDinFoo);
System.out.println("Hey, I've executed the first assignment");
getterA.apply(this).bind(getterBfromA).bind(getterCfromB).bind(getterEfromC).bind(setterEinFoo);
System.out.println("...and the second...");
getterF.apply(this).bind(getterGfromF).bind(getterHfromG).bind(getterJfromH).bind(setterJinBar);
System.out.println("...and third...");
getterF.apply(this).bind(getterGfromF).bind(getterKfromG).bind(getterMfromK).bind(setterMinBar);
System.out.println("...and fourth...");
// another more than 2000 of these expressions
System.out.println("...and we're done with every assignment we could assign...");
} <jkey>catch</jkey> {
// a superfluous catch block
}</jcode>
And, because the monadic Maybe works it does, every assignment that can occur will, and ones that cannot will be 'skipped' (by flowing NOTHING through the rest of the computation, and the proof will be in the pudding ... on the standard output will be all the statements printed.
Summary
We presented an implementation of monads in Java, with a concrete example of the Monad type: the Maybe type. We then showed that by putting a computational set into the monadic domain, the work can be performed in a type-safe manner, even with the possible presence of <jkey>nulls.</jkey> This is just one example of practical application of monadic programming in Java: the framework presented here confers the benefits of research of monadic programming in general to projects done in Java. Use the framework to discover for yourself the leverage monadic programming gives.
End notes
| | |
| [1] | Exact verbage:Phil says:January 14, 2009 at 7:01 pmI think that this could all be easily cleared up if one of you FP guys would just show us how to write one of these monad thingies in JavaâTo which a semi-mocking response was: 'you know, objects would be a lot easier for me to understand if you provided an implementation in Haskell.'Exact verbage:Cory says:April 23, 2009 at 6:26 amI may be a bit late to the game here, but Phil, that can be rephrased:I think that this could all be easily cleared up if one of you OO guys would just show us how to write one of these object thingies in HaskellâOf course you can, but it's a different type of abstraction for a different way of thinking about programmingâI write 'semi-mocking,' because: 1. OOP with message passing has been implemented in a Haskell-like language: Common Lisp. The Art of the Metaobject Protocol, a wonderful book, covers the 'traditional' object-oriented programming methodology, and its implementation, quite thoroughly and simply. |
| [2] | I leave it as an exercise to the reader to scope the Java category (Consult the Ω-calculus papers, Cardelli, et al;). |
| [3] | <jcode>Monad<Maybe, A></jcode> and <jcode>Maybe<A></jcode> are type-equivalent (but try telling the poor Java 1.6 compiler that). |
| [4] | "The same solution applies!" Geddit? Haskell is an applicative language, so the same solution applies! GEDDIT? |
| [5] | The distinction I raise here between methods and functions is the following: a method is enclosed in and owned by the defining class. A function, on the other hand, is a free-standing object and not necessarily contained in nor attached to an object. |
| [6] | Again, there is a distinction between an expression and a statement. An expression returns a value; a statement does not. A statement is purely imperative ... 'do something.' On the other hand, an expression can be purely functional ... 'do'ing nothing, as it were, e.g.: 3 + 4. A pure expression has provable properties that can be attached to it, whereas it is extremely difficult to make assertions about statements in the general sense. The upshot is that having pure (non-side-effecting) expressions in code allows us to reason about that code from a firm theoretical foundational basis. Such code is easier to test and to maintain. Side-effecting statement code make reasoning, testing and maintaining such code rather difficult. |
— about 1 in 270,000. Everyone is wowed by the rarity of the event they just witnessed.
(i.e. it is a theorem of A that f(1 + 1 + … + 1) = (source code of c)).
and compiles and returns the first such c it finds. In the case that there is no such statement, it just runs forever; similarly for the case that c fails to compile. Although cumbersome to write, I’m sure we agree that this is possible to write. If section II is not lying, then we expect that for every natural n, proofSearch n does in fact return a valid Cantor.
![\displaystyle [ 2 \times a + b \mid a \leftarrow [1,2,3] , b \leftarrow [4,5,6] , b \mathbin{\underline{\smash{\mathit{mod}}}} a == 0 ]](http://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5B+2+%5Ctimes+a+%2B+b+%5Cmid+a+%5Cleftarrow+%5B1%2C2%2C3%5D+%2C+b+%5Cleftarrow+%5B4%2C5%2C6%5D+%2C+b+%5Cmathbin%7B%5Cunderline%7B%5Csmash%7B%5Cmathit%7Bmod%7D%7D%7D%7D+a+%3D%3D+0+%5D+&bg=ffffff&fg=000000&s=0 "\displaystyle [ 2 \times a + b \mid a \leftarrow [1,2,3] , b \leftarrow [4,5,6] , b \mathbin{\underline{\smash{\mathit{mod}}}} a == 0 ]")
as 
is drawn from ![{[1,2,3]}](http://s0.wp.com/latex.php?latex=%7B%5B1%2C2%2C3%5D%7D&bg=ffffff&fg=000000&s=0 "{[1,2,3]}")
and 
from ![{[4,5,6]}](http://s0.wp.com/latex.php?latex=%7B%5B4%2C5%2C6%5D%7D&bg=ffffff&fg=000000&s=0 "{[4,5,6]}")
and such that ![{[6,7,8,8,10,12]}](http://s0.wp.com/latex.php?latex=%7B%5B6%2C7%2C8%2C8%2C10%2C12%5D%7D&bg=ffffff&fg=000000&s=0 "{[6,7,8,8,10,12]}")
.
, with a variable 
) or a filter (a boolean expression). The scope of a variable introduced by a generator extends to all subsequent generators and to the term. Note that, in contrast to the mathematical inspiration, bound variables need to be generated from some existing list.![\displaystyle \begin{array}{lcl} [ e \mid \epsilon ] &=& [e] \\ {} [ e \mid b ] &=& \mathbf{if}\;b\;\mathbf{then}\;[ e ]\;\mathbf{else}\;[\,] \\ {} [ e \mid a \leftarrow x ] &=& \mathit{map}\,(\lambda a \mathbin{.} e)\,x \\ {} [ e \mid q, q' ] &=& \mathit{concat}\,[ [ e \mid q' ] \mid q ] \end{array}](http://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7Blcl%7D+%5B+e+%5Cmid+%5Cepsilon+%5D+%26%3D%26+%5Be%5D+%5C%5C+%7B%7D+%5B+e+%5Cmid+b+%5D+%26%3D%26+%5Cmathbf%7Bif%7D%5C%3Bb%5C%3B%5Cmathbf%7Bthen%7D%5C%3B%5B+e+%5D%5C%3B%5Cmathbf%7Belse%7D%5C%3B%5B%5C%2C%5D+%5C%5C+%7B%7D+%5B+e+%5Cmid+a+%5Cleftarrow+x+%5D+%26%3D%26+%5Cmathit%7Bmap%7D%5C%2C%28%5Clambda+a+%5Cmathbin%7B.%7D+e%29%5C%2Cx+%5C%5C+%7B%7D+%5B+e+%5Cmid+q%2C+q%27+%5D+%26%3D%26+%5Cmathit%7Bconcat%7D%5C%2C%5B+%5B+e+%5Cmid+q%27+%5D+%5Cmid+q+%5D+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{lcl} [ e \mid \epsilon ] &=& [e] \\ {} [ e \mid b ] &=& \mathbf{if}\;b\;\mathbf{then}\;[ e ]\;\mathbf{else}\;[\,] \\ {} [ e \mid a \leftarrow x ] &=& \mathit{map}\,(\lambda a \mathbin{.} e)\,x \\ {} [ e \mid q, q' ] &=& \mathit{concat}\,[ [ e \mid q' ] \mid q ] \end{array}")
denotes the empty sequence of qualifiers. It’s not allowed in Haskell, but it is helpful in simplifying the translation.)![\displaystyle \begin{array}{ll} & [ 2 \times a + b \mid a \leftarrow [1,2,3] , b \leftarrow [4,5,6] , b \mathbin{\underline{\smash{\mathit{mod}}}} a == 0 ] \\ = & \mathit{concat}\,(\mathit{map}\,(\lambda a \mathbin{.} \mathit{concat}\,(\mathit{map}\,(\lambda b \mathbin{.} \mathbf{if}\;b \mathbin{\underline{\smash{\mathit{mod}}}} a == 0\;\mathbf{then}\;[2 \times a + b]\;\mathbf{else}\;[\,])\,[4,5,6]))\,[1,2,3]) \\ = & [6,7,8,8,10,12] \end{array}](http://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7Bll%7D+%26+%5B+2+%5Ctimes+a+%2B+b+%5Cmid+a+%5Cleftarrow+%5B1%2C2%2C3%5D+%2C+b+%5Cleftarrow+%5B4%2C5%2C6%5D+%2C+b+%5Cmathbin%7B%5Cunderline%7B%5Csmash%7B%5Cmathit%7Bmod%7D%7D%7D%7D+a+%3D%3D+0+%5D+%5C%5C+%3D+%26+%5Cmathit%7Bconcat%7D%5C%2C%28%5Cmathit%7Bmap%7D%5C%2C%28%5Clambda+a+%5Cmathbin%7B.%7D+%5Cmathit%7Bconcat%7D%5C%2C%28%5Cmathit%7Bmap%7D%5C%2C%28%5Clambda+b+%5Cmathbin%7B.%7D+%5Cmathbf%7Bif%7D%5C%3Bb+%5Cmathbin%7B%5Cunderline%7B%5Csmash%7B%5Cmathit%7Bmod%7D%7D%7D%7D+a+%3D%3D+0%5C%3B%5Cmathbf%7Bthen%7D%5C%3B%5B2+%5Ctimes+a+%2B+b%5D%5C%3B%5Cmathbf%7Belse%7D%5C%3B%5B%5C%2C%5D%29%5C%2C%5B4%2C5%2C6%5D%29%29%5C%2C%5B1%2C2%2C3%5D%29+%5C%5C+%3D+%26+%5B6%2C7%2C8%2C8%2C10%2C12%5D+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{ll} & [ 2 \times a + b \mid a \leftarrow [1,2,3] , b \leftarrow [4,5,6] , b \mathbin{\underline{\smash{\mathit{mod}}}} a == 0 ] \\ = & \mathit{concat}\,(\mathit{map}\,(\lambda a \mathbin{.} \mathit{concat}\,(\mathit{map}\,(\lambda b \mathbin{.} \mathbf{if}\;b \mathbin{\underline{\smash{\mathit{mod}}}} a == 0\;\mathbf{then}\;[2 \times a + b]\;\mathbf{else}\;[\,])\,[4,5,6]))\,[1,2,3]) \\ = & [6,7,8,8,10,12] \end{array}")
![\displaystyle [ e \mid p \leftarrow x ] = \mathit{concat}\,(\mathit{map}\,(\lambda a \mathbin{.} \mathbf{case}\;a\;\mathbf{of}\;p \rightarrow [ e ] \;;\; \_ \rightarrow [\,])\,x)](http://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5B+e+%5Cmid+p+%5Cleftarrow+x+%5D+%3D+%5Cmathit%7Bconcat%7D%5C%2C%28%5Cmathit%7Bmap%7D%5C%2C%28%5Clambda+a+%5Cmathbin%7B.%7D+%5Cmathbf%7Bcase%7D%5C%3Ba%5C%3B%5Cmathbf%7Bof%7D%5C%3Bp+%5Crightarrow+%5B+e+%5D+%5C%3B%3B%5C%3B+%5C_+%5Crightarrow+%5B%5C%2C%5D%29%5C%2Cx%29+&bg=ffffff&fg=000000&s=0 "\displaystyle [ e \mid p \leftarrow x ] = \mathit{concat}\,(\mathit{map}\,(\lambda a \mathbin{.} \mathbf{case}\;a\;\mathbf{of}\;p \rightarrow [ e ] \;;\; \_ \rightarrow [\,])\,x)")
![\displaystyle [ e \mid p \leftarrow x ] = \mathbf{let}\;h\,p = [ e ] ; h\,\_ = [\,]\;\mathbf{in}\; \mathit{concat}\,(\mathit{map}\,h\,x)](http://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5B+e+%5Cmid+p+%5Cleftarrow+x+%5D+%3D+%5Cmathbf%7Blet%7D%5C%3Bh%5C%2Cp+%3D+%5B+e+%5D+%3B+h%5C%2C%5C_+%3D+%5B%5C%2C%5D%5C%3B%5Cmathbf%7Bin%7D%5C%3B+%5Cmathit%7Bconcat%7D%5C%2C%28%5Cmathit%7Bmap%7D%5C%2Ch%5C%2Cx%29+&bg=ffffff&fg=000000&s=0 "\displaystyle [ e \mid p \leftarrow x ] = \mathbf{let}\;h\,p = [ e ] ; h\,\_ = [\,]\;\mathbf{in}\; \mathit{concat}\,(\mathit{map}\,h\,x)")
, singletons, 
, and the empty list. The first three are the operations arising from lists as a functor and a monad, which suggests that the same translation might be applicable to other monads too. But the fourth ingredient, the empty list, does not come from the functor and monad structures; that requires an extra assumption: 
![\displaystyle \begin{array}{lcl} [ e \mid \epsilon ] &=& \mathit{return}\,e \\ {} [ e \mid b ] &=& \mathbf{if}\;b\;\mathbf{then}\;\mathit{return}\,e\;\mathbf{else}\;\mathit{mzero} \\ {} [ e \mid p \leftarrow m ] &=& \mathbf{let}\;h\,p = \mathit{return}\,e ; h\,\_ = \mathit{mzero}\;\mathbf{in}\; \mathit{join}\,(\mathit{map}\,h\,m) \\ {} [ e \mid q, q' ] &=& \mathit{join}\,[ [ e \mid q' ] \mid q ] \end{array}](http://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7Blcl%7D+%5B+e+%5Cmid+%5Cepsilon+%5D+%26%3D%26+%5Cmathit%7Breturn%7D%5C%2Ce+%5C%5C+%7B%7D+%5B+e+%5Cmid+b+%5D+%26%3D%26+%5Cmathbf%7Bif%7D%5C%3Bb%5C%3B%5Cmathbf%7Bthen%7D%5C%3B%5Cmathit%7Breturn%7D%5C%2Ce%5C%3B%5Cmathbf%7Belse%7D%5C%3B%5Cmathit%7Bmzero%7D+%5C%5C+%7B%7D+%5B+e+%5Cmid+p+%5Cleftarrow+m+%5D+%26%3D%26+%5Cmathbf%7Blet%7D%5C%3Bh%5C%2Cp+%3D+%5Cmathit%7Breturn%7D%5C%2Ce+%3B+h%5C%2C%5C_+%3D+%5Cmathit%7Bmzero%7D%5C%3B%5Cmathbf%7Bin%7D%5C%3B+%5Cmathit%7Bjoin%7D%5C%2C%28%5Cmathit%7Bmap%7D%5C%2Ch%5C%2Cm%29+%5C%5C+%7B%7D+%5B+e+%5Cmid+q%2C+q%27+%5D+%26%3D%26+%5Cmathit%7Bjoin%7D%5C%2C%5B+%5B+e+%5Cmid+q%27+%5D+%5Cmid+q+%5D+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{lcl} [ e \mid \epsilon ] &=& \mathit{return}\,e \\ {} [ e \mid b ] &=& \mathbf{if}\;b\;\mathbf{then}\;\mathit{return}\,e\;\mathbf{else}\;\mathit{mzero} \\ {} [ e \mid p \leftarrow m ] &=& \mathbf{let}\;h\,p = \mathit{return}\,e ; h\,\_ = \mathit{mzero}\;\mathbf{in}\; \mathit{join}\,(\mathit{map}\,h\,m) \\ {} [ e \mid q, q' ] &=& \mathit{join}\,[ [ e \mid q' ] \mid q ] \end{array}")
![{[ e \mid \epsilon ] = [ e \mid \mathit{True} ]}](http://s0.wp.com/latex.php?latex=%7B%5B+e+%5Cmid+%5Cepsilon+%5D+%3D+%5B+e+%5Cmid+%5Cmathit%7BTrue%7D+%5D%7D&bg=ffffff&fg=000000&s=0 "{[ e \mid \epsilon ] = [ e \mid \mathit{True} ]}")
). The actual monad to be used is implicit; if we want to be explicit, we could use a subscript, as in “![{[ e \mid q ]_\mathsf{List}}](http://s0.wp.com/latex.php?latex=%7B%5B+e+%5Cmid+q+%5D_%5Cmathsf%7BList%7D%7D&bg=ffffff&fg=000000&s=0 "{[ e \mid q ]_\mathsf{List}}")
“.
method of the 
class in the first case, and the 
method of the 
class in the second). I think it is neater to have a monad subclass 
with a single method subsuming both these operators. Of course, this does mean that the translation forces a monad comprehension with filters or possibly failing generators to be interpreted in a monad in the 
. 
![\displaystyle [ e \mid a \leftarrow \mathit{mzero} ] = \mathit{mzero}](http://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5B+e+%5Cmid+a+%5Cleftarrow+%5Cmathit%7Bmzero%7D+%5D+%3D+%5Cmathit%7Bmzero%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle [ e \mid a \leftarrow \mathit{mzero} ] = \mathit{mzero}")
, which is a kind of sequential composition.)
of at most one element, any comprehension using generators of the form 
will only yield another such collection, whereas the union of two one-element collections will in general have two elements.
: 
![\displaystyle [ e \mid a \leftarrow m \uplus n, q ] = [ e \mid a \leftarrow m, q ] \uplus [ e \mid a \leftarrow n, q ]](http://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5B+e+%5Cmid+a+%5Cleftarrow+m+%5Cuplus+n%2C+q+%5D+%3D+%5B+e+%5Cmid+a+%5Cleftarrow+m%2C+q+%5D+%5Cuplus+%5B+e+%5Cmid+a+%5Cleftarrow+n%2C+q+%5D+&bg=ffffff&fg=000000&s=0 "\displaystyle [ e \mid a \leftarrow m \uplus n, q ] = [ e \mid a \leftarrow m, q ] \uplus [ e \mid a \leftarrow n, q ]")
” for “
is the intersection of the two parent classes 
such that 
and 
. In particular, 
is itself a monad algebra. When the monad is also a ringad, 
such that 
(exercise!). Without loss of generality, we write 
for 
is a ringad algebra.![{[ e \mid q ]^\oplus}](http://s0.wp.com/latex.php?latex=%7B%5B+e+%5Cmid+q+%5D%5E%5Coplus%7D&bg=ffffff&fg=000000&s=0 "{[ e \mid q ]^\oplus}")
“; although this doesn’t add much, because we could just have written “![{\oplus/\,[e \mid q]}](http://s0.wp.com/latex.php?latex=%7B%5Coplus%2F%5C%2C%5Be+%5Cmid+q%5D%7D&bg=ffffff&fg=000000&s=0 "{\oplus/\,[e \mid q]}")
” instead. We could generalize from reductions 
; but this doesn’t add much either, because the map is easily combined with the comprehension—it’s easy to show the “map over comprehension” property ![\displaystyle \mathit{map}\,f\,[e \mid q] = [f\,e \mid q]](http://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cmathit%7Bmap%7D%5C%2Cf%5C%2C%5Be+%5Cmid+q%5D+%3D+%5Bf%5C%2Ce+%5Cmid+q%5D+&bg=ffffff&fg=000000&s=0 "\displaystyle \mathit{map}\,f\,[e \mid q] = [f\,e \mid q]")
; such an 
. (So, although ![{[a^2 \mid a \leftarrow x, \mathit{odd}\,a]_\mathsf{Bag}^{+}}](http://s0.wp.com/latex.php?latex=%7B%5Ba%5E2+%5Cmid+a+%5Cleftarrow+x%2C+%5Cmathit%7Bodd%7D%5C%2Ca%5D_%5Cmathsf%7BBag%7D%5E%7B%2B%7D%7D&bg=ffffff&fg=000000&s=0 "{[a^2 \mid a \leftarrow x, \mathit{odd}\,a]_\mathsf{Bag}^{+}}")
denotes the sum of the squares of the odd elements of bag ![{[a^2 \mid a \leftarrow x, \mathit{odd}\,a]_\mathsf{Set}^{+}}](http://s0.wp.com/latex.php?latex=%7B%5Ba%5E2+%5Cmid+a+%5Cleftarrow+x%2C+%5Cmathit%7Bodd%7D%5C%2Ca%5D_%5Cmathsf%7BSet%7D%5E%7B%2B%7D%7D&bg=ffffff&fg=000000&s=0 "{[a^2 \mid a \leftarrow x, \mathit{odd}\,a]_\mathsf{Set}^{+}}")
(with 
is not idempotent.) In particular, 
must be the unit of 
. ![\displaystyle [ e \mid q ]^\oplus = \oplus/\,[e \mid q]](http://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5B+e+%5Cmid+q+%5D%5E%5Coplus+%3D+%5Coplus%2F%5C%2C%5Be+%5Cmid+q%5D+&bg=ffffff&fg=000000&s=0 "\displaystyle [ e \mid q ]^\oplus = \oplus/\,[e \mid q]")
![\displaystyle \begin{array}{ll} & [ e \mid \epsilon ]^\oplus \\ = & \qquad \{ \mbox{aggregation} \} \\ & \oplus/\,[ e \mid \epsilon ] \\ = & \qquad \{ \mbox{comprehension} \} \\ & \oplus/\,(\mathit{return}\,e) \\ = & \qquad \{ \mbox{monad algebra} \} \\ & e \end{array}](http://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7Bll%7D+%26+%5B+e+%5Cmid+%5Cepsilon+%5D%5E%5Coplus+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Baggregation%7D+%5C%7D+%5C%5C+%26+%5Coplus%2F%5C%2C%5B+e+%5Cmid+%5Cepsilon+%5D+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Bcomprehension%7D+%5C%7D+%5C%5C+%26+%5Coplus%2F%5C%2C%28%5Cmathit%7Breturn%7D%5C%2Ce%29+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Bmonad+algebra%7D+%5C%7D+%5C%5C+%26+e+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{ll} & [ e \mid \epsilon ]^\oplus \\ = & \qquad \{ \mbox{aggregation} \} \\ & \oplus/\,[ e \mid \epsilon ] \\ = & \qquad \{ \mbox{comprehension} \} \\ & \oplus/\,(\mathit{return}\,e) \\ = & \qquad \{ \mbox{monad algebra} \} \\ & e \end{array}")
![\displaystyle \begin{array}{ll} & [ e \mid b ]^\oplus \\ = & \qquad \{ \mbox{aggregation} \} \\ & \oplus/\,[ e \mid b ] \\ = & \qquad \{ \mbox{comprehension} \} \\ & \oplus/\,(\mathbf{if}\;b\;\mathbf{then}\;\mathit{return}\,e\;\mathbf{else}\;\emptyset) \\ = & \qquad \{ \mbox{lift out the conditional} \} \\ & \mathbf{if}\;b\;\mathbf{then}\;{\oplus/}\,(\mathit{return}\,e)\;\mathbf{else}\;{\oplus/}\,\emptyset \\ = & \qquad \{ \mbox{ringad algebra} \} \\ & \mathbf{if}\;b\;\mathbf{then}\;e\;\mathbf{else}\;1_\oplus \end{array}](http://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7Bll%7D+%26+%5B+e+%5Cmid+b+%5D%5E%5Coplus+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Baggregation%7D+%5C%7D+%5C%5C+%26+%5Coplus%2F%5C%2C%5B+e+%5Cmid+b+%5D+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Bcomprehension%7D+%5C%7D+%5C%5C+%26+%5Coplus%2F%5C%2C%28%5Cmathbf%7Bif%7D%5C%3Bb%5C%3B%5Cmathbf%7Bthen%7D%5C%3B%5Cmathit%7Breturn%7D%5C%2Ce%5C%3B%5Cmathbf%7Belse%7D%5C%3B%5Cemptyset%29+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Blift+out+the+conditional%7D+%5C%7D+%5C%5C+%26+%5Cmathbf%7Bif%7D%5C%3Bb%5C%3B%5Cmathbf%7Bthen%7D%5C%3B%7B%5Coplus%2F%7D%5C%2C%28%5Cmathit%7Breturn%7D%5C%2Ce%29%5C%3B%5Cmathbf%7Belse%7D%5C%3B%7B%5Coplus%2F%7D%5C%2C%5Cemptyset+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Bringad+algebra%7D+%5C%7D+%5C%5C+%26+%5Cmathbf%7Bif%7D%5C%3Bb%5C%3B%5Cmathbf%7Bthen%7D%5C%3Be%5C%3B%5Cmathbf%7Belse%7D%5C%3B1_%5Coplus+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{ll} & [ e \mid b ]^\oplus \\ = & \qquad \{ \mbox{aggregation} \} \\ & \oplus/\,[ e \mid b ] \\ = & \qquad \{ \mbox{comprehension} \} \\ & \oplus/\,(\mathbf{if}\;b\;\mathbf{then}\;\mathit{return}\,e\;\mathbf{else}\;\emptyset) \\ = & \qquad \{ \mbox{lift out the conditional} \} \\ & \mathbf{if}\;b\;\mathbf{then}\;{\oplus/}\,(\mathit{return}\,e)\;\mathbf{else}\;{\oplus/}\,\emptyset \\ = & \qquad \{ \mbox{ringad algebra} \} \\ & \mathbf{if}\;b\;\mathbf{then}\;e\;\mathbf{else}\;1_\oplus \end{array}")
![\displaystyle \begin{array}{ll} & [ e \mid p \leftarrow m ]^\oplus \\ = & \qquad \{ \mbox{aggregation} \} \\ & \oplus/\,[ e \mid p \leftarrow m ] \\ = & \qquad \{ \mbox{comprehension} \} \\ & \oplus/\,(\mathbf{let}\;h\,p = \mathit{return}\,e ; h\,\_ = \emptyset\;\mathbf{in}\;\mathit{join}\,(\mathit{map}\,h\,m)) \\ = & \qquad \{ \mbox{lift out the \textbf{let}} \} \\ & \mathbf{let}\;h\,p = \mathit{return},e ; h\,\_ = \emptyset\;\mathbf{in}\;{\oplus/}\,(\mathit{join}\,(\mathit{map}\,h\,m)) \\ = & \qquad \{ \mbox{monad algebra} \} \\ & \mathbf{let}\;h\,p = \mathit{return}\,e ; h\,\_ = \emptyset\;\mathbf{in}\;{\oplus/}\,(\mathit{map}\,(\oplus/)\,(\mathit{map}\,h\,m)) \\ = & \qquad \{ \mbox{functors} \} \\ & \mathbf{let}\;h\,p = \mathit{return}\,e ; h\,\_ = \emptyset\;\mathbf{in}\;{\oplus/}\,(\mathit{map}\,(\oplus/ \cdot h)\,m) \\ = & \qquad \{ \mbox{let \(h' = \oplus/ \cdot h\)} \} \\ & \mathbf{let}\;h'\,p = \oplus/\,(\mathit{return}\,e) ; h'\,\_ = \oplus/\,\emptyset\;\mathbf{in}\;{\oplus/}\,(\mathit{map}\,h'\,m) \\ = & \qquad \{ \mbox{ringad algebra} \} \\ & \mathbf{let}\;h'\,p = e ; h'\,\_ = 1_\oplus\;\mathbf{in}\;{\oplus/}\,(\mathit{map}\,h'\,m) \end{array}](http://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7Bll%7D+%26+%5B+e+%5Cmid+p+%5Cleftarrow+m+%5D%5E%5Coplus+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Baggregation%7D+%5C%7D+%5C%5C+%26+%5Coplus%2F%5C%2C%5B+e+%5Cmid+p+%5Cleftarrow+m+%5D+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Bcomprehension%7D+%5C%7D+%5C%5C+%26+%5Coplus%2F%5C%2C%28%5Cmathbf%7Blet%7D%5C%3Bh%5C%2Cp+%3D+%5Cmathit%7Breturn%7D%5C%2Ce+%3B+h%5C%2C%5C_+%3D+%5Cemptyset%5C%3B%5Cmathbf%7Bin%7D%5C%3B%5Cmathit%7Bjoin%7D%5C%2C%28%5Cmathit%7Bmap%7D%5C%2Ch%5C%2Cm%29%29+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Blift+out+the+%5Ctextbf%7Blet%7D%7D+%5C%7D+%5C%5C+%26+%5Cmathbf%7Blet%7D%5C%3Bh%5C%2Cp+%3D+%5Cmathit%7Breturn%7D%2Ce+%3B+h%5C%2C%5C_+%3D+%5Cemptyset%5C%3B%5Cmathbf%7Bin%7D%5C%3B%7B%5Coplus%2F%7D%5C%2C%28%5Cmathit%7Bjoin%7D%5C%2C%28%5Cmathit%7Bmap%7D%5C%2Ch%5C%2Cm%29%29+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Bmonad+algebra%7D+%5C%7D+%5C%5C+%26+%5Cmathbf%7Blet%7D%5C%3Bh%5C%2Cp+%3D+%5Cmathit%7Breturn%7D%5C%2Ce+%3B+h%5C%2C%5C_+%3D+%5Cemptyset%5C%3B%5Cmathbf%7Bin%7D%5C%3B%7B%5Coplus%2F%7D%5C%2C%28%5Cmathit%7Bmap%7D%5C%2C%28%5Coplus%2F%29%5C%2C%28%5Cmathit%7Bmap%7D%5C%2Ch%5C%2Cm%29%29+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Bfunctors%7D+%5C%7D+%5C%5C+%26+%5Cmathbf%7Blet%7D%5C%3Bh%5C%2Cp+%3D+%5Cmathit%7Breturn%7D%5C%2Ce+%3B+h%5C%2C%5C_+%3D+%5Cemptyset%5C%3B%5Cmathbf%7Bin%7D%5C%3B%7B%5Coplus%2F%7D%5C%2C%28%5Cmathit%7Bmap%7D%5C%2C%28%5Coplus%2F+%5Ccdot+h%29%5C%2Cm%29+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Blet+%5C%28h%27+%3D+%5Coplus%2F+%5Ccdot+h%5C%29%7D+%5C%7D+%5C%5C+%26+%5Cmathbf%7Blet%7D%5C%3Bh%27%5C%2Cp+%3D+%5Coplus%2F%5C%2C%28%5Cmathit%7Breturn%7D%5C%2Ce%29+%3B+h%27%5C%2C%5C_+%3D+%5Coplus%2F%5C%2C%5Cemptyset%5C%3B%5Cmathbf%7Bin%7D%5C%3B%7B%5Coplus%2F%7D%5C%2C%28%5Cmathit%7Bmap%7D%5C%2Ch%27%5C%2Cm%29+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Bringad+algebra%7D+%5C%7D+%5C%5C+%26+%5Cmathbf%7Blet%7D%5C%3Bh%27%5C%2Cp+%3D+e+%3B+h%27%5C%2C%5C_+%3D+1_%5Coplus%5C%3B%5Cmathbf%7Bin%7D%5C%3B%7B%5Coplus%2F%7D%5C%2C%28%5Cmathit%7Bmap%7D%5C%2Ch%27%5C%2Cm%29+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{ll} & [ e \mid p \leftarrow m ]^\oplus \\ = & \qquad \{ \mbox{aggregation} \} \\ & \oplus/\,[ e \mid p \leftarrow m ] \\ = & \qquad \{ \mbox{comprehension} \} \\ & \oplus/\,(\mathbf{let}\;h\,p = \mathit{return}\,e ; h\,\_ = \emptyset\;\mathbf{in}\;\mathit{join}\,(\mathit{map}\,h\,m)) \\ = & \qquad \{ \mbox{lift out the \textbf{let}} \} \\ & \mathbf{let}\;h\,p = \mathit{return},e ; h\,\_ = \emptyset\;\mathbf{in}\;{\oplus/}\,(\mathit{join}\,(\mathit{map}\,h\,m)) \\ = & \qquad \{ \mbox{monad algebra} \} \\ & \mathbf{let}\;h\,p = \mathit{return}\,e ; h\,\_ = \emptyset\;\mathbf{in}\;{\oplus/}\,(\mathit{map}\,(\oplus/)\,(\mathit{map}\,h\,m)) \\ = & \qquad \{ \mbox{functors} \} \\ & \mathbf{let}\;h\,p = \mathit{return}\,e ; h\,\_ = \emptyset\;\mathbf{in}\;{\oplus/}\,(\mathit{map}\,(\oplus/ \cdot h)\,m) \\ = & \qquad \{ \mbox{let \(h' = \oplus/ \cdot h\)} \} \\ & \mathbf{let}\;h'\,p = \oplus/\,(\mathit{return}\,e) ; h'\,\_ = \oplus/\,\emptyset\;\mathbf{in}\;{\oplus/}\,(\mathit{map}\,h'\,m) \\ = & \qquad \{ \mbox{ringad algebra} \} \\ & \mathbf{let}\;h'\,p = e ; h'\,\_ = 1_\oplus\;\mathbf{in}\;{\oplus/}\,(\mathit{map}\,h'\,m) \end{array}")
![\displaystyle \begin{array}{ll} & [ e \mid q, q' ]^\oplus \\ = & \qquad \{ \mbox{aggregation} \} \\ & \oplus/\,[ e \mid q, q' ] \\ = & \qquad \{ \mbox{comprehension} \} \\ & \oplus/\,(\mathit{join}\,[ [ e \mid q'] \mid q ] \\ = & \qquad \{ \mbox{monad algebra} \} \\ & \oplus/\,(\mathit{map}\,(\oplus/)\,[ [ e \mid q'] \mid q ]) \\ = & \qquad \{ \mbox{map over comprehension} \} \\ & \oplus/\,[ \oplus/\,[ e \mid q'] \mid q ] \\ = & \qquad \{ \mbox{aggregation} \} \\ & [ [ e \mid q']^\oplus \mid q ]^\oplus \end{array}](http://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7Bll%7D+%26+%5B+e+%5Cmid+q%2C+q%27+%5D%5E%5Coplus+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Baggregation%7D+%5C%7D+%5C%5C+%26+%5Coplus%2F%5C%2C%5B+e+%5Cmid+q%2C+q%27+%5D+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Bcomprehension%7D+%5C%7D+%5C%5C+%26+%5Coplus%2F%5C%2C%28%5Cmathit%7Bjoin%7D%5C%2C%5B+%5B+e+%5Cmid+q%27%5D+%5Cmid+q+%5D+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Bmonad+algebra%7D+%5C%7D+%5C%5C+%26+%5Coplus%2F%5C%2C%28%5Cmathit%7Bmap%7D%5C%2C%28%5Coplus%2F%29%5C%2C%5B+%5B+e+%5Cmid+q%27%5D+%5Cmid+q+%5D%29+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Bmap+over+comprehension%7D+%5C%7D+%5C%5C+%26+%5Coplus%2F%5C%2C%5B+%5Coplus%2F%5C%2C%5B+e+%5Cmid+q%27%5D+%5Cmid+q+%5D+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Baggregation%7D+%5C%7D+%5C%5C+%26+%5B+%5B+e+%5Cmid+q%27%5D%5E%5Coplus+%5Cmid+q+%5D%5E%5Coplus+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{ll} & [ e \mid q, q' ]^\oplus \\ = & \qquad \{ \mbox{aggregation} \} \\ & \oplus/\,[ e \mid q, q' ] \\ = & \qquad \{ \mbox{comprehension} \} \\ & \oplus/\,(\mathit{join}\,[ [ e \mid q'] \mid q ] \\ = & \qquad \{ \mbox{monad algebra} \} \\ & \oplus/\,(\mathit{map}\,(\oplus/)\,[ [ e \mid q'] \mid q ]) \\ = & \qquad \{ \mbox{map over comprehension} \} \\ & \oplus/\,[ \oplus/\,[ e \mid q'] \mid q ] \\ = & \qquad \{ \mbox{aggregation} \} \\ & [ [ e \mid q']^\oplus \mid q ]^\oplus \end{array}")
![\displaystyle \begin{array}{lcl} [ e \mid \epsilon ]^\oplus &=& e \\ {} [ e \mid b ]^\oplus &=&\mathbf{if}\;b\;\mathbf{then}\;e\;\mathbf{else}\;1_\oplus \\ {} [ e \mid p \leftarrow m ]^\oplus &=& \mathbf{let}\;h\,p = e ; h\,\_ = 1_\oplus\;\mathbf{in}\;{\oplus/}\,(\mathit{map}\,h\,m) \\ {} [ e \mid q, q' ]^\oplus &=& [ [ e \mid q']^\oplus \mid q ]^\oplus \end{array}](http://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7Blcl%7D+%5B+e+%5Cmid+%5Cepsilon+%5D%5E%5Coplus+%26%3D%26+e+%5C%5C+%7B%7D+%5B+e+%5Cmid+b+%5D%5E%5Coplus+%26%3D%26%5Cmathbf%7Bif%7D%5C%3Bb%5C%3B%5Cmathbf%7Bthen%7D%5C%3Be%5C%3B%5Cmathbf%7Belse%7D%5C%3B1_%5Coplus+%5C%5C+%7B%7D+%5B+e+%5Cmid+p+%5Cleftarrow+m+%5D%5E%5Coplus+%26%3D%26+%5Cmathbf%7Blet%7D%5C%3Bh%5C%2Cp+%3D+e+%3B+h%5C%2C%5C_+%3D+1_%5Coplus%5C%3B%5Cmathbf%7Bin%7D%5C%3B%7B%5Coplus%2F%7D%5C%2C%28%5Cmathit%7Bmap%7D%5C%2Ch%5C%2Cm%29+%5C%5C+%7B%7D+%5B+e+%5Cmid+q%2C+q%27+%5D%5E%5Coplus+%26%3D%26+%5B+%5B+e+%5Cmid+q%27%5D%5E%5Coplus+%5Cmid+q+%5D%5E%5Coplus+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{lcl} [ e \mid \epsilon ]^\oplus &=& e \\ {} [ e \mid b ]^\oplus &=&\mathbf{if}\;b\;\mathbf{then}\;e\;\mathbf{else}\;1_\oplus \\ {} [ e \mid p \leftarrow m ]^\oplus &=& \mathbf{let}\;h\,p = e ; h\,\_ = 1_\oplus\;\mathbf{in}\;{\oplus/}\,(\mathit{map}\,h\,m) \\ {} [ e \mid q, q' ]^\oplus &=& [ [ e \mid q']^\oplus \mid q ]^\oplus \end{array}")
![{[a^2 \mid a \leftarrow x, \mathit{odd}\,a]_\mathsf{Set}}](http://s0.wp.com/latex.php?latex=%7B%5Ba%5E2+%5Cmid+a+%5Cleftarrow+x%2C+%5Cmathit%7Bodd%7D%5C%2Ca%5D_%5Cmathsf%7BSet%7D%7D&bg=ffffff&fg=000000&s=0 "{[a^2 \mid a \leftarrow x, \mathit{odd}\,a]_\mathsf{Set}}")
denotes (the set of) the squares of the odd elements of (the set) ![{[a^2 \mid a \leftarrow x, \mathit{odd}\,a]_\mathsf{Bag}}](http://s0.wp.com/latex.php?latex=%7B%5Ba%5E2+%5Cmid+a+%5Cleftarrow+x%2C+%5Cmathit%7Bodd%7D%5C%2Ca%5D_%5Cmathsf%7BBag%7D%7D&bg=ffffff&fg=000000&s=0 "{[a^2 \mid a \leftarrow x, \mathit{odd}\,a]_\mathsf{Bag}}")
denotes the bag of such elements, with 
and 
, a monad morphism 
is a natural transformation 
—that is, a family 
of arrows, coherent in the sense that 
for 
—that also preserves the monad structure: 
is a monad morphism 
![\displaystyle \begin{array}{ll} & \phi\,[ e \mid \epsilon ]_\mathsf{M} \\ = & \qquad \{ \mbox{comprehension} \} \\ & \phi\,(\mathit{return}_\mathsf{M}\,e) \\ = & \qquad \{ \mbox{ringad morphism} \} \\ & \mathit{return}_\mathsf{N}\,e \\ = & \qquad \{ \mbox{comprehension} \} \\ & [e \mid \epsilon ]_\mathsf{N} \end{array}](http://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7Bll%7D+%26+%5Cphi%5C%2C%5B+e+%5Cmid+%5Cepsilon+%5D_%5Cmathsf%7BM%7D+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Bcomprehension%7D+%5C%7D+%5C%5C+%26+%5Cphi%5C%2C%28%5Cmathit%7Breturn%7D_%5Cmathsf%7BM%7D%5C%2Ce%29+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Bringad+morphism%7D+%5C%7D+%5C%5C+%26+%5Cmathit%7Breturn%7D_%5Cmathsf%7BN%7D%5C%2Ce+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Bcomprehension%7D+%5C%7D+%5C%5C+%26+%5Be+%5Cmid+%5Cepsilon+%5D_%5Cmathsf%7BN%7D+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{ll} & \phi\,[ e \mid \epsilon ]_\mathsf{M} \\ = & \qquad \{ \mbox{comprehension} \} \\ & \phi\,(\mathit{return}_\mathsf{M}\,e) \\ = & \qquad \{ \mbox{ringad morphism} \} \\ & \mathit{return}_\mathsf{N}\,e \\ = & \qquad \{ \mbox{comprehension} \} \\ & [e \mid \epsilon ]_\mathsf{N} \end{array}")
![\displaystyle \begin{array}{ll} & \phi\,[ e \mid b ]_\mathsf{M} \\ = & \qquad \{ \mbox{comprehension} \} \\ & \phi\,(\mathbf{if}\;b\;\mathbf{then}\;\mathit{return}_\mathsf{M}\,e\;\mathbf{else}\;\emptyset_\mathsf{M}) \\ = & \qquad \{ \mbox{lift out the conditional} \} \\ & \mathbf{if}\;b\;\mathbf{then}\;\phi\,(\mathit{return}_\mathsf{M}\,e)\;\mathbf{else}\;\phi\,\emptyset_\mathsf{M} \\ = & \qquad \{ \mbox{ringad morphism} \} \\ & \mathbf{if}\;b\;\mathbf{then}\;\mathit{return}_\mathsf{N}\,e\;\mathbf{else}\;\emptyset_\mathsf{N} \\ = & \qquad \{ \mbox{comprehension} \} \\ & [ e \mid b ]_\mathsf{N} \end{array}](http://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7Bll%7D+%26+%5Cphi%5C%2C%5B+e+%5Cmid+b+%5D_%5Cmathsf%7BM%7D+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Bcomprehension%7D+%5C%7D+%5C%5C+%26+%5Cphi%5C%2C%28%5Cmathbf%7Bif%7D%5C%3Bb%5C%3B%5Cmathbf%7Bthen%7D%5C%3B%5Cmathit%7Breturn%7D_%5Cmathsf%7BM%7D%5C%2Ce%5C%3B%5Cmathbf%7Belse%7D%5C%3B%5Cemptyset_%5Cmathsf%7BM%7D%29+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Blift+out+the+conditional%7D+%5C%7D+%5C%5C+%26+%5Cmathbf%7Bif%7D%5C%3Bb%5C%3B%5Cmathbf%7Bthen%7D%5C%3B%5Cphi%5C%2C%28%5Cmathit%7Breturn%7D_%5Cmathsf%7BM%7D%5C%2Ce%29%5C%3B%5Cmathbf%7Belse%7D%5C%3B%5Cphi%5C%2C%5Cemptyset_%5Cmathsf%7BM%7D+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Bringad+morphism%7D+%5C%7D+%5C%5C+%26+%5Cmathbf%7Bif%7D%5C%3Bb%5C%3B%5Cmathbf%7Bthen%7D%5C%3B%5Cmathit%7Breturn%7D_%5Cmathsf%7BN%7D%5C%2Ce%5C%3B%5Cmathbf%7Belse%7D%5C%3B%5Cemptyset_%5Cmathsf%7BN%7D+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Bcomprehension%7D+%5C%7D+%5C%5C+%26+%5B+e+%5Cmid+b+%5D_%5Cmathsf%7BN%7D+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{ll} & \phi\,[ e \mid b ]_\mathsf{M} \\ = & \qquad \{ \mbox{comprehension} \} \\ & \phi\,(\mathbf{if}\;b\;\mathbf{then}\;\mathit{return}_\mathsf{M}\,e\;\mathbf{else}\;\emptyset_\mathsf{M}) \\ = & \qquad \{ \mbox{lift out the conditional} \} \\ & \mathbf{if}\;b\;\mathbf{then}\;\phi\,(\mathit{return}_\mathsf{M}\,e)\;\mathbf{else}\;\phi\,\emptyset_\mathsf{M} \\ = & \qquad \{ \mbox{ringad morphism} \} \\ & \mathbf{if}\;b\;\mathbf{then}\;\mathit{return}_\mathsf{N}\,e\;\mathbf{else}\;\emptyset_\mathsf{N} \\ = & \qquad \{ \mbox{comprehension} \} \\ & [ e \mid b ]_\mathsf{N} \end{array}")
![\displaystyle \begin{array}{ll} & \phi\,[ e \mid p \leftarrow m ]_\mathsf{M} \\ = & \qquad \{ \mbox{comprehension} \} \\ & \phi\,(\mathbf{let}\;h\,p = \mathit{return}_\mathsf{M}\,e ; h\,\_ = \emptyset_\mathsf{M}\;\mathbf{in}\;\mathit{join}_\mathsf{M}\,(\mathit{map}_\mathsf{M}\,h\,m)) \\ = & \qquad \{ \mbox{lift out the \textbf{let}} \} \\ & \mathbf{let}\;h\,p = \mathit{return}_\mathsf{M}\,e ; h\,\_ = \emptyset_\mathsf{M}\;\mathbf{in}\;\phi\,(\mathit{join}_\mathsf{M}\,(\mathit{map}_\mathsf{M}\,h\,m)) \\ = & \qquad \{ \mbox{ringad morphism, functors} \} \\ & \mathbf{let}\;h\,p = \mathit{return}_\mathsf{M}\,e ; h\,\_ = \emptyset_\mathsf{M}\;\mathbf{in}\;\mathit{join}_\mathsf{N}\,(\phi\,(\mathit{map}_\mathsf{M}\,(\phi \cdot h)\,m)) \\ = & \qquad \{ \mbox{let \(h' = \phi \cdot h\)} \} \\ & \mathbf{let}\;h'\,p = \phi\,(\mathit{return}_\mathsf{M}\,e) ; h'\,\_ = \phi\,\emptyset_\mathsf{M}\;\mathbf{in}\;\mathit{join}_\mathsf{N}\,(\phi\,(\mathit{map}_\mathsf{M}\,h'\,m)) \\ = & \qquad \{ \mbox{ringad morphism, induction} \} \\ & \mathbf{let}\;h'\,p = \mathit{return}_\mathsf{N}\,e ; h'\,\_ = \emptyset_\mathsf{N}\;\mathbf{in}\;\mathit{join}_\mathsf{N}\,(\phi\,(\mathit{map}_\mathsf{M}\,h'\,m)) \\ = & \qquad \{ \mbox{naturality of \(\phi\)} \} \\ & \mathbf{let}\;h'\,p = \mathit{return}_\mathsf{N}\,e ; h'\,\_ = \emptyset_\mathsf{N}\;\mathbf{in}\;\mathit{join}_\mathsf{N}\,(\mathit{map}_\mathsf{N}\,h'\,(\phi\,m)) \\ = & \qquad \{ \mbox{comprehension} \} \\ & [ e \mid p \leftarrow \phi\,m ]_\mathsf{N} \end{array}](http://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7Bll%7D+%26+%5Cphi%5C%2C%5B+e+%5Cmid+p+%5Cleftarrow+m+%5D_%5Cmathsf%7BM%7D+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Bcomprehension%7D+%5C%7D+%5C%5C+%26+%5Cphi%5C%2C%28%5Cmathbf%7Blet%7D%5C%3Bh%5C%2Cp+%3D+%5Cmathit%7Breturn%7D_%5Cmathsf%7BM%7D%5C%2Ce+%3B+h%5C%2C%5C_+%3D+%5Cemptyset_%5Cmathsf%7BM%7D%5C%3B%5Cmathbf%7Bin%7D%5C%3B%5Cmathit%7Bjoin%7D_%5Cmathsf%7BM%7D%5C%2C%28%5Cmathit%7Bmap%7D_%5Cmathsf%7BM%7D%5C%2Ch%5C%2Cm%29%29+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Blift+out+the+%5Ctextbf%7Blet%7D%7D+%5C%7D+%5C%5C+%26+%5Cmathbf%7Blet%7D%5C%3Bh%5C%2Cp+%3D+%5Cmathit%7Breturn%7D_%5Cmathsf%7BM%7D%5C%2Ce+%3B+h%5C%2C%5C_+%3D+%5Cemptyset_%5Cmathsf%7BM%7D%5C%3B%5Cmathbf%7Bin%7D%5C%3B%5Cphi%5C%2C%28%5Cmathit%7Bjoin%7D_%5Cmathsf%7BM%7D%5C%2C%28%5Cmathit%7Bmap%7D_%5Cmathsf%7BM%7D%5C%2Ch%5C%2Cm%29%29+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Bringad+morphism%2C+functors%7D+%5C%7D+%5C%5C+%26+%5Cmathbf%7Blet%7D%5C%3Bh%5C%2Cp+%3D+%5Cmathit%7Breturn%7D_%5Cmathsf%7BM%7D%5C%2Ce+%3B+h%5C%2C%5C_+%3D+%5Cemptyset_%5Cmathsf%7BM%7D%5C%3B%5Cmathbf%7Bin%7D%5C%3B%5Cmathit%7Bjoin%7D_%5Cmathsf%7BN%7D%5C%2C%28%5Cphi%5C%2C%28%5Cmathit%7Bmap%7D_%5Cmathsf%7BM%7D%5C%2C%28%5Cphi+%5Ccdot+h%29%5C%2Cm%29%29+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Blet+%5C%28h%27+%3D+%5Cphi+%5Ccdot+h%5C%29%7D+%5C%7D+%5C%5C+%26+%5Cmathbf%7Blet%7D%5C%3Bh%27%5C%2Cp+%3D+%5Cphi%5C%2C%28%5Cmathit%7Breturn%7D_%5Cmathsf%7BM%7D%5C%2Ce%29+%3B+h%27%5C%2C%5C_+%3D+%5Cphi%5C%2C%5Cemptyset_%5Cmathsf%7BM%7D%5C%3B%5Cmathbf%7Bin%7D%5C%3B%5Cmathit%7Bjoin%7D_%5Cmathsf%7BN%7D%5C%2C%28%5Cphi%5C%2C%28%5Cmathit%7Bmap%7D_%5Cmathsf%7BM%7D%5C%2Ch%27%5C%2Cm%29%29+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Bringad+morphism%2C+induction%7D+%5C%7D+%5C%5C+%26+%5Cmathbf%7Blet%7D%5C%3Bh%27%5C%2Cp+%3D+%5Cmathit%7Breturn%7D_%5Cmathsf%7BN%7D%5C%2Ce+%3B+h%27%5C%2C%5C_+%3D+%5Cemptyset_%5Cmathsf%7BN%7D%5C%3B%5Cmathbf%7Bin%7D%5C%3B%5Cmathit%7Bjoin%7D_%5Cmathsf%7BN%7D%5C%2C%28%5Cphi%5C%2C%28%5Cmathit%7Bmap%7D_%5Cmathsf%7BM%7D%5C%2Ch%27%5C%2Cm%29%29+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Bnaturality+of+%5C%28%5Cphi%5C%29%7D+%5C%7D+%5C%5C+%26+%5Cmathbf%7Blet%7D%5C%3Bh%27%5C%2Cp+%3D+%5Cmathit%7Breturn%7D_%5Cmathsf%7BN%7D%5C%2Ce+%3B+h%27%5C%2C%5C_+%3D+%5Cemptyset_%5Cmathsf%7BN%7D%5C%3B%5Cmathbf%7Bin%7D%5C%3B%5Cmathit%7Bjoin%7D_%5Cmathsf%7BN%7D%5C%2C%28%5Cmathit%7Bmap%7D_%5Cmathsf%7BN%7D%5C%2Ch%27%5C%2C%28%5Cphi%5C%2Cm%29%29+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Bcomprehension%7D+%5C%7D+%5C%5C+%26+%5B+e+%5Cmid+p+%5Cleftarrow+%5Cphi%5C%2Cm+%5D_%5Cmathsf%7BN%7D+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{ll} & \phi\,[ e \mid p \leftarrow m ]_\mathsf{M} \\ = & \qquad \{ \mbox{comprehension} \} \\ & \phi\,(\mathbf{let}\;h\,p = \mathit{return}_\mathsf{M}\,e ; h\,\_ = \emptyset_\mathsf{M}\;\mathbf{in}\;\mathit{join}_\mathsf{M}\,(\mathit{map}_\mathsf{M}\,h\,m)) \\ = & \qquad \{ \mbox{lift out the \textbf{let}} \} \\ & \mathbf{let}\;h\,p = \mathit{return}_\mathsf{M}\,e ; h\,\_ = \emptyset_\mathsf{M}\;\mathbf{in}\;\phi\,(\mathit{join}_\mathsf{M}\,(\mathit{map}_\mathsf{M}\,h\,m)) \\ = & \qquad \{ \mbox{ringad morphism, functors} \} \\ & \mathbf{let}\;h\,p = \mathit{return}_\mathsf{M}\,e ; h\,\_ = \emptyset_\mathsf{M}\;\mathbf{in}\;\mathit{join}_\mathsf{N}\,(\phi\,(\mathit{map}_\mathsf{M}\,(\phi \cdot h)\,m)) \\ = & \qquad \{ \mbox{let \(h' = \phi \cdot h\)} \} \\ & \mathbf{let}\;h'\,p = \phi\,(\mathit{return}_\mathsf{M}\,e) ; h'\,\_ = \phi\,\emptyset_\mathsf{M}\;\mathbf{in}\;\mathit{join}_\mathsf{N}\,(\phi\,(\mathit{map}_\mathsf{M}\,h'\,m)) \\ = & \qquad \{ \mbox{ringad morphism, induction} \} \\ & \mathbf{let}\;h'\,p = \mathit{return}_\mathsf{N}\,e ; h'\,\_ = \emptyset_\mathsf{N}\;\mathbf{in}\;\mathit{join}_\mathsf{N}\,(\phi\,(\mathit{map}_\mathsf{M}\,h'\,m)) \\ = & \qquad \{ \mbox{naturality of \(\phi\)} \} \\ & \mathbf{let}\;h'\,p = \mathit{return}_\mathsf{N}\,e ; h'\,\_ = \emptyset_\mathsf{N}\;\mathbf{in}\;\mathit{join}_\mathsf{N}\,(\mathit{map}_\mathsf{N}\,h'\,(\phi\,m)) \\ = & \qquad \{ \mbox{comprehension} \} \\ & [ e \mid p \leftarrow \phi\,m ]_\mathsf{N} \end{array}")
![\displaystyle \begin{array}{ll} & \phi\,[ e \mid q, q' ]_\mathsf{M} \\ = & \qquad \{ \mbox{comprehension} \} \\ & \phi\,(\mathit{join}\,[ [ e \mid q' ]_\mathsf{M} \mid q ]_\mathsf{M}) \\ = & \qquad \{ \mbox{ringad morphism} \} \\ & \phi\,(\mathit{map}\,\phi\,[ [ e \mid q' ]_\mathsf{M} \mid q ]_\mathsf{M}) \\ = & \qquad \{ \mbox{map over comprehension} \} \\ & \phi\,[ \phi\,[ e \mid q' ]_\mathsf{M} \mid q ]_\mathsf{M} \\ = & \qquad \{ \mbox{induction} \} \\ & [ [ e \mid q' ]_\mathsf{N} \mid q ]_\mathsf{N} \\ = & \qquad \{ \mbox{comprehension} \} \\ & [ e \mid q, q' ]_\mathsf{N} \end{array}](http://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7Bll%7D+%26+%5Cphi%5C%2C%5B+e+%5Cmid+q%2C+q%27+%5D_%5Cmathsf%7BM%7D+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Bcomprehension%7D+%5C%7D+%5C%5C+%26+%5Cphi%5C%2C%28%5Cmathit%7Bjoin%7D%5C%2C%5B+%5B+e+%5Cmid+q%27+%5D_%5Cmathsf%7BM%7D+%5Cmid+q+%5D_%5Cmathsf%7BM%7D%29+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Bringad+morphism%7D+%5C%7D+%5C%5C+%26+%5Cphi%5C%2C%28%5Cmathit%7Bmap%7D%5C%2C%5Cphi%5C%2C%5B+%5B+e+%5Cmid+q%27+%5D_%5Cmathsf%7BM%7D+%5Cmid+q+%5D_%5Cmathsf%7BM%7D%29+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Bmap+over+comprehension%7D+%5C%7D+%5C%5C+%26+%5Cphi%5C%2C%5B+%5Cphi%5C%2C%5B+e+%5Cmid+q%27+%5D_%5Cmathsf%7BM%7D+%5Cmid+q+%5D_%5Cmathsf%7BM%7D+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Binduction%7D+%5C%7D+%5C%5C+%26+%5B+%5B+e+%5Cmid+q%27+%5D_%5Cmathsf%7BN%7D+%5Cmid+q+%5D_%5Cmathsf%7BN%7D+%5C%5C+%3D+%26+%5Cqquad+%5C%7B+%5Cmbox%7Bcomprehension%7D+%5C%7D+%5C%5C+%26+%5B+e+%5Cmid+q%2C+q%27+%5D_%5Cmathsf%7BN%7D+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{ll} & \phi\,[ e \mid q, q' ]_\mathsf{M} \\ = & \qquad \{ \mbox{comprehension} \} \\ & \phi\,(\mathit{join}\,[ [ e \mid q' ]_\mathsf{M} \mid q ]_\mathsf{M}) \\ = & \qquad \{ \mbox{ringad morphism} \} \\ & \phi\,(\mathit{map}\,\phi\,[ [ e \mid q' ]_\mathsf{M} \mid q ]_\mathsf{M}) \\ = & \qquad \{ \mbox{map over comprehension} \} \\ & \phi\,[ \phi\,[ e \mid q' ]_\mathsf{M} \mid q ]_\mathsf{M} \\ = & \qquad \{ \mbox{induction} \} \\ & [ [ e \mid q' ]_\mathsf{N} \mid q ]_\mathsf{N} \\ = & \qquad \{ \mbox{comprehension} \} \\ & [ e \mid q, q' ]_\mathsf{N} \end{array}")
is the obvious ringad morphism from bags to sets, discarding information about the multiplicity of repeated elements, and ![\displaystyle \mathit{bag2set}\,[a^2 \mid a \leftarrow x, \mathit{odd}\,a]_\mathsf{Bag} = [a^2 \mid a \leftarrow \mathit{bag2set}\,x, \mathit{odd}\,a]_\mathsf{Set}](http://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cmathit%7Bbag2set%7D%5C%2C%5Ba%5E2+%5Cmid+a+%5Cleftarrow+x%2C+%5Cmathit%7Bodd%7D%5C%2Ca%5D_%5Cmathsf%7BBag%7D+%3D+%5Ba%5E2+%5Cmid+a+%5Cleftarrow+%5Cmathit%7Bbag2set%7D%5C%2Cx%2C+%5Cmathit%7Bodd%7D%5C%2Ca%5D_%5Cmathsf%7BSet%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \mathit{bag2set}\,[a^2 \mid a \leftarrow x, \mathit{odd}\,a]_\mathsf{Bag} = [a^2 \mid a \leftarrow \mathit{bag2set}\,x, \mathit{odd}\,a]_\mathsf{Set}")
. This would allow us to write, for example, ![\displaystyle [ a+b \mid a \leftarrow [1,2,3], b \leftarrow \langle4,4,5\rangle ]_\mathsf{Set} = \{ 5,6,7,8 \}](http://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5B+a%2Bb+%5Cmid+a+%5Cleftarrow+%5B1%2C2%2C3%5D%2C+b+%5Cleftarrow+%5Clangle4%2C4%2C5%5Crangle+%5D_%5Cmathsf%7BSet%7D+%3D+%5C%7B+5%2C6%2C7%2C8+%5C%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle [ a+b \mid a \leftarrow [1,2,3], b \leftarrow \langle4,4,5\rangle ]_\mathsf{Set} = \{ 5,6,7,8 \}")
for the extension of a bag), instead of the more pedantic ![\displaystyle [ a+b \mid a \leftarrow \mathit{list2set}\,[1,2,3], b \leftarrow \mathit{bag2set}\,\langle4,4,5\rangle ]_\mathsf{Set} = \{ 5,6,7,8 \}](http://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5B+a%2Bb+%5Cmid+a+%5Cleftarrow+%5Cmathit%7Blist2set%7D%5C%2C%5B1%2C2%2C3%5D%2C+b+%5Cleftarrow+%5Cmathit%7Bbag2set%7D%5C%2C%5Clangle4%2C4%2C5%5Crangle+%5D_%5Cmathsf%7BSet%7D+%3D+%5C%7B+5%2C6%2C7%2C8+%5C%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle [ a+b \mid a \leftarrow \mathit{list2set}\,[1,2,3], b \leftarrow \mathit{bag2set}\,\langle4,4,5\rangle ]_\mathsf{Set} = \{ 5,6,7,8 \}")
,
.
,
.
.
.
. In the meantime, if you have a go, please let me know what you come up with. In particular, if anything behaves badly, please shout – I want this version to work well! 
.
.
,
.
.
.
operator: ![\displaystyle \begin{array}{lcl} \mathit{scanl} &::& (\beta \rightarrow \alpha \rightarrow \beta) \rightarrow \beta \rightarrow [\alpha] \rightarrow [\beta] \\ \mathit{scanl}\,f\,e\,[\,] &=& [e] \\ \mathit{scanl}\,f\,e\,(a:x) &=& e : \mathit{scanl}\,f\,(f\,e\,a)\,x \medskip \\ \mathit{totals} &::& [{\mathbb Z}] \rightarrow [{\mathbb Z}] \\ \mathit{totals} &=& \mathit{scanl}\,(+)\,0 \end{array}](http://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7Blcl%7D+%5Cmathit%7Bscanl%7D+%26%3A%3A%26+%28%5Cbeta+%5Crightarrow+%5Calpha+%5Crightarrow+%5Cbeta%29+%5Crightarrow+%5Cbeta+%5Crightarrow+%5B%5Calpha%5D+%5Crightarrow+%5B%5Cbeta%5D+%5C%5C+%5Cmathit%7Bscanl%7D%5C%2Cf%5C%2Ce%5C%2C%5B%5C%2C%5D+%26%3D%26+%5Be%5D+%5C%5C+%5Cmathit%7Bscanl%7D%5C%2Cf%5C%2Ce%5C%2C%28a%3Ax%29+%26%3D%26+e+%3A+%5Cmathit%7Bscanl%7D%5C%2Cf%5C%2C%28f%5C%2Ce%5C%2Ca%29%5C%2Cx+%5Cmedskip+%5C%5C+%5Cmathit%7Btotals%7D+%26%3A%3A%26+%5B%7B%5Cmathbb+Z%7D%5D+%5Crightarrow+%5B%7B%5Cmathbb+Z%7D%5D+%5C%5C+%5Cmathit%7Btotals%7D+%26%3D%26+%5Cmathit%7Bscanl%7D%5C%2C%28%2B%29%5C%2C0+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{lcl} \mathit{scanl} &::& (\beta \rightarrow \alpha \rightarrow \beta) \rightarrow \beta \rightarrow [\alpha] \rightarrow [\beta] \\ \mathit{scanl}\,f\,e\,[\,] &=& [e] \\ \mathit{scanl}\,f\,e\,(a:x) &=& e : \mathit{scanl}\,f\,(f\,e\,a)\,x \medskip \\ \mathit{totals} &::& [{\mathbb Z}] \rightarrow [{\mathbb Z}] \\ \mathit{totals} &=& \mathit{scanl}\,(+)\,0 \end{array}")
function, and it too is an instance of ![\displaystyle \mathit{inits} = \mathit{scanl}\,\mathit{snoc}\,[\,] \quad\mathbf{where}\; \mathit{snoc}\,x\,a = x \mathbin{{+}\!\!\!{+}} [a]](http://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cmathit%7Binits%7D+%3D+%5Cmathit%7Bscanl%7D%5C%2C%5Cmathit%7Bsnoc%7D%5C%2C%5B%5C%2C%5D+%5Cquad%5Cmathbf%7Bwhere%7D%5C%3B+%5Cmathit%7Bsnoc%7D%5C%2Cx%5C%2Ca+%3D+x+%5Cmathbin%7B%7B%2B%7D%5C%21%5C%21%5C%21%7B%2B%7D%7D+%5Ba%5D+&bg=ffffff&fg=000000&s=0 "\displaystyle \mathit{inits} = \mathit{scanl}\,\mathit{snoc}\,[\,] \quad\mathbf{where}\; \mathit{snoc}\,x\,a = x \mathbin{{+}\!\!\!{+}} [a]")
applied to that node’s predecessors. Read from right to left, the scan lemma is an efficiency-improving transformation, eliminating duplicate computations; but note that this only works on expressions 
where 
is a 
, 
, and 
, and identifying the relationships between them. Conversely, one can view 
yields the root of a tree: 
are the nodes labelled 
. One could represent those ancestors simply as a list, ![{[2,4,3]}](http://s0.wp.com/latex.php?latex=%7B%5B2%2C4%2C3%5D%7D&bg=ffffff&fg=000000&s=0 "{[2,4,3]}")
; but that rules out the possibility of a downwards accumulation treating left children differently from right children, which is essential in a number of algorithms (such as the parallel prefix and tree drawing algorithms in my thesis). A more faithful rendering is to define a new datatype of paths that captures the left and right turns—a kind of non-empty cons list, but with both a “left cons” and a “right cons” constructor: 
. I leave it as an exercise for the more energetic reader to work out a definition for 
.
labels every node of a data structure of type 
with the descendants of that node, and still the case that the descendants form a data structure also of type 
. However, in general, the datatype 
does not allow for a label at every node, so we need the labelled variant 
where 
. Then we can define 
returns the root label of a labelled data structure—by construction, every labelled data structure has a root label—and 
is the unique arrow to the unit type. Moreover, we get a datatype-generic 
operator, and a Scan Lemma: 
datatype above, to represent the “ancestors” of a node in an inductive datatype. The tricky bit is that data structures in general are non-linear—a node may have many children—whereas paths are linear—every node has exactly one child, except the last which has none; how can we define a “linear version” 
of 
? Technically, we might say that a functor is linear (actually, “affine” would be a better word) if it distributes over sum.
is either 
, 
, or some constant type such as 
or 
. For example, for leaf-labelled binary trees 
, so 
(there are two variants), 
(the first variant has a single literal, 
(the second variant has two literals, 
we define a 
-ary functor 
, where 
is the “degree of branching” of variant 
, which is the number of 
for which 
), in such a way that 
is “the next unused 
” when 
of paths, as the inductive datatype of shape 
where 
, which records the “local content” of a node (its shape and labels, but without any of its children). Every other element of the path consists of the local content of a node together with an indication of which direction to go next; this amounts to the choice of a variant 
of variant 
and a family of “cons” constructors 
for 
and 
.
which labels every node with its descendants, we can define a function 
to label every node with its ancestors, in the form of the path to that node. One definition is as a fold; informally, at each stage we construct a singleton path to the root, and map the appropriate “cons” over the paths to each node in each of the children (see the paper for a concrete definition). This is inefficient, because of the repeated maps; it’s analogous to defining ![\displaystyle \begin{array}{lcl} \mathit{inits}\,[\,] &=& [[\,]] \\ \mathit{inits}\,(a:x) &=& [\,] : \mathit{map}\,(a:)\,(\mathit{inits}\,x) \end{array}](http://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7Blcl%7D+%5Cmathit%7Binits%7D%5C%2C%5B%5C%2C%5D+%26%3D%26+%5B%5B%5C%2C%5D%5D+%5C%5C+%5Cmathit%7Binits%7D%5C%2C%28a%3Ax%29+%26%3D%26+%5B%5C%2C%5D+%3A+%5Cmathit%7Bmap%7D%5C%2C%28a%3A%29%5C%2C%28%5Cmathit%7Binits%7D%5C%2Cx%29+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{lcl} \mathit{inits}\,[\,] &=& [[\,]] \\ \mathit{inits}\,(a:x) &=& [\,] : \mathit{map}\,(a:)\,(\mathit{inits}\,x) \end{array}")
the “path so far”; this avoids the maps, but it is still quadratic because there are no common subexpressions among the various paths. (This is analogous to an accumulating-parameter definition of ![\displaystyle \begin{array}{lcl} \mathit{inits} &=& \mathit{inits}'\,\mathit{id} \medskip \\ \mathit{inits}'\,f\,[\,] &=& f\,[\,] \\ \mathit{inits}'\,f\,(a:x) &=& f\,[\,] : \mathit{inits}'\,(f \cdot (a:))\,x \end{array}](http://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7Blcl%7D+%5Cmathit%7Binits%7D+%26%3D%26+%5Cmathit%7Binits%7D%27%5C%2C%5Cmathit%7Bid%7D+%5Cmedskip+%5C%5C+%5Cmathit%7Binits%7D%27%5C%2Cf%5C%2C%5B%5C%2C%5D+%26%3D%26+f%5C%2C%5B%5C%2C%5D+%5C%5C+%5Cmathit%7Binits%7D%27%5C%2Cf%5C%2C%28a%3Ax%29+%26%3D%26+f%5C%2C%5B%5C%2C%5D+%3A+%5Cmathit%7Binits%7D%27%5C%2C%28f+%5Ccdot+%28a%3A%29%29%5C%2Cx+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{lcl} \mathit{inits} &=& \mathit{inits}'\,\mathit{id} \medskip \\ \mathit{inits}'\,f\,[\,] &=& f\,[\,] \\ \mathit{inits}'\,f\,(a:x) &=& f\,[\,] : \mathit{inits}'\,(f \cdot (a:))\,x \end{array}")
. It is defined as an unfold, with a body 
of type 
of applying the body will be constructed from two components, of types 
and 
: the first gives the root label of the accumulation and the seeds for processing the children, and the second gives the children themselves. 
-structures of the same shape.
, it unpacks the 
, and discards the 
and the 
is the labelled variant of 
, where 
. We then suppose as a parameter to the accumulation a function 
to complete the construction of the first component. In order that the two components can be zipped together, we require that 
is the unique function to the unit type. Then, although the 
, it will still itself be total.
of a functor 
is like 
, but with precisely one 
of 
, which breaks an 
is that it really is an annotation—if you throw away the annotations, you get back what you started with: 
of bifunctors differentiable in their second argument, along with 
, which turns a tree into a labelled tree of paths. We will write it with an accumulating parameter, representing the “path so far”: ![\displaystyle \begin{array}{lcl} \mathit{paths}_\mathsf{F} &::& \mathsf{T}\alpha \rightarrow \mathsf{L}(\mathsf{P}\alpha) \\ \mathit{paths}_\mathsf{F}\,t &=& \mathit{paths}'_\mathsf{F}\,(t,[\,]) \end{array}](http://s0.wp.com/latex.php?latex=%5Cdisplaystyle++%5Cbegin%7Barray%7D%7Blcl%7D+%5Cmathit%7Bpaths%7D_%5Cmathsf%7BF%7D+%26%3A%3A%26+%5Cmathsf%7BT%7D%5Calpha+%5Crightarrow+%5Cmathsf%7BL%7D%28%5Cmathsf%7BP%7D%5Calpha%29+%5C%5C+%5Cmathit%7Bpaths%7D_%5Cmathsf%7BF%7D%5C%2Ct+%26%3D%26+%5Cmathit%7Bpaths%7D%27_%5Cmathsf%7BF%7D%5C%2C%28t%2C%5B%5C%2C%5D%29+%5Cend%7Barray%7D+&bg=ffffff&fg=000000&s=0 "\displaystyle \begin{array}{lcl} \mathit{paths}_\mathsf{F} &::& \mathsf{T}\alpha \rightarrow \mathsf{L}(\mathsf{P}\alpha) \\ \mathit{paths}_\mathsf{F}\,t &=& \mathit{paths}'_\mathsf{F}\,(t,[\,]) \end{array}")
of a tree and a path 
to its root, 
must construct the corresponding labelled tree of paths. Since 
and 
. For the first component of this pair we will use 
s, consing each one-hole context onto 
take constant time. 
