Rant against charitable organizations (and solution)

I happen to be an highly optimistic person. That's a good thing.

Sometimes, my less optimistic friends think the world is a terrible place to live in. Thankfully, they're wrong, so I can cheer them up by pointing out solutions to the problems they perceive. Given this ability, I think I'd make a great volunteer at one of those teen help hotlines. The problem is, none of them wants my help! Well, none that I could find in my area, anyway.

You see, I never donate to charitable organizations. I think it's dumb to give an organization money so that someone else can help people out and get paid for it. I say, cut the middle man! Let me give you a hand instead.

And you know what they replied? "Great, we do have some volunteer positions available. Your task would be to call people and ask them for donations. Interested?"

They really don't want us concerned citizens to help. Like everybody else, they just want our money.

And of course, being the resourceful optimist that I am, I've got a solution to that. And of course, being the enthusiastic developer that I am, my solution involves building a website.

An ordinary charitable organization would use its website to tell you about its plans for solving the problems of the world, and to request your "help" (that is, your money) for implementing that plan. On my hypothetical website, I would ask you about your plan for solving the problems of the world. And I would show you the plans of the other users, so you can contact them and contribute if you think the plan is worth trying.

Most importantly, the plans would be highly detailed. Where ordinary charitable organizations would merely draw a pie chart showing how they allocate your money, our plans would tell you exactly which actions we want to see performed, and why each action contributes to (a sub-goal which contributes to a sub-goal which contributes to) resolving the issue at hand, say, "ending world hunger".

One of the reasons for using such detailed plans is to convince visitors that our plan will actually succeed. I think there is a tendency to assume that, by default, big organizations know what they are doing, and we can't compete with that bias unless we show that we know what we are doing.

And for those of us who don't know what we're doing, we can always ask for the help of our creative contributors. As a project grows, it should become more and more complete, more and more plausible, and attract more and more contributors. If it doesn't, then it probably wasn't a very good idea to begin with.

The other reason for writing highly detailed plans is to keep track of progress. At the most-detailed level, a plan should consist of concrete actions which individuals can perform. That way, resourceful visitors who are convinced by a plan will be able to contribute by performing the concrete action, and ticking it off as completed.

The idea of empowering the community by replacing big organizations with self-organizing teams of volunteers is not new; I've merely translated existing ideas from the world of software to the world of charity. What I'm promoting, it seems, could be called Open Source Charity. (or "Open Plan", perhaps?)

And what this means, is you don't even have to wait for me to implement the aforementioned website. If you have an idea that could change the world, then just use your favourite issue tracking system, and start organizing issues into a concrete plan. Easy enough, right? The world has plenty of good things as it is, like I've claimed.

Well, have fun making the world a better place. Good luck!

well-foundedness, part 2 of 2: code is data. or is it codata?

Whether it is represented as finite strings or as finite trees, code is finite, and thus code is data, not codata. That should settle the question.

haskell code = 2 + 3 * 4 haskell string_data = "2 + 3 * 4" haskell data Exp = Lit Int | Add Exp Exp | Mul Exp Exp haskell tree_data = Add (Lit 2) (Mul (Lit 3) (Lit 4))

Except, of course, that's not really the question I wanted to ask. In my very first post, I warned that manipulating code as raw strings or trees was a bit primitive, and I've since been taught an alternative: higher-order abstract syntax. For the purpose of this post, that basically means I'm representing the code using a function instead of a data-structure.

With data-structures, proofs are usually done using structural induction (see part 1). But when using a function to represent code, what could be its internal structure? What are its substructures?

The clue lies in the exponential notation for function types. But first, remember the familiar multiplicative notation for, well, product types. If (a, b, c) is a value of type A × B × C, then b would be a substructure of type B. That seems reasonable. Now, consider a function λx. f x of type A → B. The exponential notation for this type is B^A = B × B × ... × B, with one occurrence of B per inhabitant of A. If these inhabitants are (a₀, a₁, ...), then an alternate representation of our function could be (f a₀, f a₁, ...). This expanded form contains exactly the same information as the lambda notation, it's just a lot more verbose, especially when A has infinitely many inhabitants.

Seeing this explicit notation, an immediate conclusion is that for any value a of the appropriate type, the (value corresponding to the) application f a is a substructure of f. Wow! It was totally unexpected for me. That's why I'm writing about it. To share my excitement. But don't get too excited yet: there's a warning coming up.

I have mildly motivated our search for substructures in functions with the relatively exciting perspective of creating a structural induction proof whose decreasing structures include functions. Well, I hope you're not that motivated, because you can't do that. Function application isn't well-founded at all, at least in some languages. Take the identity function, for example. In Haskell, it is possible to apply the identity function to itself. The resulting substructure, obviously, will be the identity function. But that substructure also has the identity function as a substructure, and by continuing to recur in this fashion, we will never reach a base case. The proof will instead go on, forever, in an infinite regress.

Uh? I hope you're surprised! How could structural induction work with all of those other kinds of substructure relations, yet fail with this one? What's so special about functions?

Let's pause to ponder the presumed absurdity of an infinitely-nested structure. Take lists, for example. They are finite because after a finite number of elements, we reach the end of the list. An infinitely-nested list would go on forever, cons after cons, never reaching an end. While this would be absurd in most programming languages, infinite lists are actually commonplace in Haskell... So maybe functions aren't so unique after all!

Functions and infinite lists are examples of codata, and induction is indeed known not to work with those. Expressions of infinite depth do not have a terminating evaluation; the evaluator can't even read the entire input! I hear we're supposed to use "coinduction" instead, but I can't comment on that technique yet. What I can say, however, is that even though Haskell allows data and codata to mix, it's apparently a bad idea, and there are languages with type systems strong enough to prevent it. In these languages, there are two distinct types for lists, but I haven't seen a distinct type for "cofunctions" yet. I suspect that a function must be codata whenever some of its possible return values are.

Well, I bet you've heard enough about well-founded and non-well-founded structures (data and codata) for your entire life. But personally, I think I'm just getting started.

well-foundedness, part 1 of 2: who cares?

If you're like me, you've often heard of well-foundedness, but never really bothered to learn what it really meant nor why it's important. If you're like most people, on the other hand, then you've never even heard the word and you couldn't care less. Well, go ahead, skip this post. You'll be back and eager to learn once you try and fail to read part 2.

...see? I told you you'd be back. Since you're presumably only interested in understanding enough about well-foundedness in order to follow part 2, I might as well use the same example: a little expression language for evaluating numerical expressions such as 2 + 3 * 4.

haskell data Exp = Lit Int | Add Exp Exp | Mul Exp Exp haskell eval :: Exp -> Int haskell eval (Lit n) = n haskell eval (Add e1 e2) = eval e1 + eval e2 haskell eval (Mul e1 e2) = eval e1 * eval e2 haskell eval (Add (Lit 2) (Mul (Lit 3) (Lit 4)))

Since there are no looping constructs in this simple language, it's reasonable to expect evaluation to always terminate. It's possible to prove so using traditional induction, say, on the height of the expression tree. Induction arguments are routine in mathematics, and thus the previous statement is usually all that is needed in order to convince another mathematician that the eval function always terminates; but since today's post is about different kinds of induction, I'll flesh out the proof so you can see the difference.

proof: by (traditional) induction on the height of the expression tree. Base case: if the tree has height one, i.e. if it is a leaf, then the expression is a literal number of the form Lit n and the evaluation terminates immediately by returning n. For the induction step, suppose eval e terminates for all expressions e of height strictly less than n. We wish to show that eval also terminates on expressions of height exactly n. There are two cases: expressions of the form Add e1 e2 and expressions of the form Mul e1 e2. In either case, e1 and e2 are subtrees of the entire expression, and thus have a strictly smaller height. By the induction hypothesis, eval e1 and eval e2 both terminate, and thus the expressions eval e1 + eval e2 and eval e1 * eval e2 also terminate (assuming Haskell's numeric primitives do). ☐

There are other versions of the above argument which are equally valid. For example, instead of the expression depth, we could use the expression size, meaning the number of constructors (Lit, Add and Mul) used to construct the expression.

haskell size :: Exp -> Int haskell size (Lit n) = 1 haskell size (Add e1 e2) = 1 + size e1 + size e2 haskell size (Mul e1 e2) = 1 + size e1 * size e2

This metric is also smaller for e1 and e2 than for Add e1 e2 and Mul e1 e2, so the induction step will succeed.

The two variants I have discussed so far use numbers (depth, size) to argue termination. The idea is that the base case proves the statement to be true when the number is one, and then the induction step can use this fact to prove that the statement is also true when the number is two. This new fact can in turn be used to prove the statement when the number is three, after which we can handle case four, then case five, and so on. In the end, we'll have a proof for all numbers, meaning that expressions of all sizes and depths have a terminating evaluation.

An alternative view of induction is to begin with a statement with a particular number, say five, about which we are actually interested. The induction step gives us a conditional proof of the statement, which depends on the statement to be true for the number four. But the statement is true for the number four, because it's true for three, because it's true for two, because it's true for one. And the statement is true for one because the base case proves so.

This second view is even a bit more "efficient" than the first, because we don't actually need to decrement so slowly. Add (Lit 2) (Mul (Lit 3) (Lit 4)), of size 5, has a terminating evaluation because Lit 2 and Mul (Lit 3) (Lit 4), of sizes 1 and 3, also terminate; the first by the base case, the second because Lit 3 and Lit 4 terminate. The last two expressions had size 1 and are also proved to terminate by the base case. Notice that we managed not to discuss expressions of size 2 and 4 at all.

Using the more efficient version, we see that the proof for n doesn't need to recur on n-1, but can actually use any m as long as m < n. We can generalize further. Even though induction traditionally uses the less-than relation of natural numbers, it is totally possible to find other suitable relations. Structural induction, for instance, says that the expression e1 is less than expression Add e1 e2 because the latter contains e1 as a sub-expression.

This structural less-than is very different from the numerical less-than. For one thing, the numerical less-than is total, meaning that given two numbers, one of the two is going to be smaller than (or equal to) the other. With structures such as Add (Lit 1) (Lit 2) and Mul (Lit 3) (Lit 4), neither is contained within the other, so the structural less-than isn't total. But while our intuitive, everyday notion of ordering seems to require totality, the notion isn't required by the induction principle.

One notion which is required, however, is (you guessed it) well-foundedness. The property basically states that when recurring on smaller and smaller values, we will hit the base case after finitely many steps. This is required: otherwise, the proof could go on and on and on without the sceptics even being convinced.

Speaking of sceptics: are you convinced that well-foundedness is a useful concept now?

God exists (with probability one)

Bonjour Gab. Joyeux Noël. C'est un jour tout particulier pour toi, alors profites-en.

Tu n'aimes pas quand, à la messe de minuit, les imposteurs envahissent ton église pour prier maladroitement à tes côtés, alors je ne prétendrai pas partager ton enthousiasme. Par contre, je voulais te rappeler que moi aussi je crois en dieu — juste pas en Dieu, avec une majuscule. Tu dois te dire que je dis ça pour te faire plaisir. Qu'à mes amis athéistes, je dis le contraire avec autant de conviction. Eh bien en fait... ouain, ça ressemble pas mal à ça.

Et c'est pourquoi ce post est, en quelque sorte, un cadeau de Noël. Pour toi, je fais l'effort de choisir un camp officiel et de l'afficher clairement. Bon, peut-être pas aussi clairement que si je l'avais mis sur Facebook, mais en tout cas c'est là où on arrive quand on tape mon nom sur Google ces temps-ci.

Le reste du post est mon argument "anthropique" que tu connais déjà. Alors, si tu préfères profiter du reste de la journée pour penser au petit Jésus et profiter de Noël, c'est un moment idéal pour fermer cette fenêtre.

---

The above French comment isn't necessary to understand the following argument. Feel free to disagree violently with my hypotheses or with my reasoning.

The first of these wild hypotheses is that mathematical truths actually exist, in some parallel Platonic world of ideas. My actual belief is stronger: in a twisted interpretation of modal logic, I believe that necessary truths, such as mathematical tautologies, necessarily exist; whereas the facts about our universe are merely ordinarily true, and therefore physical things only happen to exist. I have been led to these unusual beliefs by a convincing argument using the anthropic principle, which I will not repeat here.

Now that we accept the hypothesis, we have to accept a very, very large number of existing things. True statements about numbers. True statements about sets. True statements about true statements. True statements about programs. True statements about programs running games. True statements about a program running an extremely realistic simulation of our physical universe. True statements, one for each instant, describing the entire contents of the simulated universe at that instant. Oh, did I mention that I also assume that our universe is both computable and indistinguishable from a simulation of itself?

At this point I usually picture the statements in the sequence of universe contents to be shown true one after the other, unfolding the story of the universe at the rate at which we feel it happening. But I have come to realize that time is a universe-specific concept, making it implausible to imagine time flowing by in the world of ideas. Because of this, I must admit that I'm not sure how consciousness should enter the picture, but at this point I am at least reasonably sure that (a possibly consciousness-less version of) our universe exists (what a relief!), and even necessarily exists.

An atheist would stop here and point out that since the universe necessarily exists, there is no need to postulate a god powerful enough to bring it into existence. And I totally agree. Nothing so far has argued for or against the existence of a god. Against the lack of evidence, some people (like me!) prefer to assume a god-less model by default, while others prefer to stick to their own favorite meme. But some of us reason one step further.

My next guest in this series of implausible hypotheses is that some humble universe inhabitants are so powerful that they count as gods in their own right. In my book a god is an entity which creates, maintains, and possibly interacts with one or more universe(s). And since I've already assumed that our universe could be nothing more than a simulation, a god could be little more than a programmer with infinite time on his hands. One can certainly imagine a universe similar to ours in which this was true, a universe which would also necessarily exist. In fact, some of us claim that our universe is itself suitable for setting up the kind of infinite computation which running sub-universes require.

With infinite time on his hands, it's not at all a waste for him to run all finite universes, one after the other, until the non-existing end of time. Surprisingly, it's also possible to run all infinite universes, if he interleaves them cleverly. And while you can't assume that god's unsearchable ways will involve enumerating all programs, we've got so many gods in our collection of necessarily existing universes that I'm sure we can find one who likes to do just that.

Running every possibility, god will eventually create a sub-universe looking just like ours and one just like his, in which a sub-god will be running sub-sub-universes including one like ours and one like his, and so on. We end up with infinitely many identical copies of god, and most importantly, infinitely many identical copies of universes indistinguishable from ours.

Let's recapitulate. We have now established the existence of many, many worlds, some of them like ours, some of them different. At the top level are infinitely many of them, all distinct. One of them is indistinguishable from ours. Infinitely many are extremely close to ours, like the many-worlds of quantum mechanics, but not exactly the same. Those top-level worlds exist by virtue of the first hypothesis, the existence of the world of ideas. Again, nothing so far encourages or precludes a pre-top-level god who created that world, so I default to a god-less model. In addition to the single top-level world which is like ours, infinitely many others exist as sub-universes, created by something in a higher-level universe. Those universes do have some sort of god, namely, that thing which created them. It could very well be a machine without a programmer, or a programmer without a machine.

Many-world models are suitable for probabilistic arguments. For example, if a many-world theory postulates a particular distribution of worlds, it should be possible to calculate the conditional probability of an universe having such and such property given that intelligent beings inhabit it. This could be used to make observable predictions about our universe, and test the theory. Today, however, I'm going to be lame and make a non-observable prediction: the conditional probability of an universe being god-less, given that it is indistinguishable from ours, is zero. After all, there is only one such god-less universe, the one at the top level, divided by infinitely many equally probable indistinguishable universes. Hence, god exists with probability one.

Non-standard inhabitants

The goal of this post is to demonstrate that I'm not crazy. One of my latest discoveries involves a function called "inhabitants", but that's impossible, so says the textbooks, and I can't explain my discovery any further because I crumble under the mathematically rigorous objections. You know, the way researchers whose latest discovery involves a perpetual motion engine tend not to be taken very seriously.

So I took the time to read about those mathematically rigorous objections, and I'm happy to report that my conclusion is that I am not a crackpot. It's just a misunderstanding. A bit as if my perpetual motion engine was supposed to cycle more slowly at every turn, without ever stopping (hence the name) and without producing useful work. It may or may not be an interesting discovery, but it has nothing to do with what people usually call perpetual motion engines.

Now that I'm convinced of my own sanity, the hard part is to convince others. I'll practice with you, foreign and unknown readers, who are probably too far away to cause me trouble if I fail.

First of, I'd like to explain what people usually mean by "inhabitants". The type inhabitation problem is the task of determining, for any given type in a particular programming language, whether there exists an expression in that language which has that type. Such an expression is said to "inhabit" its type. It would be even more useful if an actual inhabitant could be returned as a witness, and that's precisely what Djinn does for Haskell's type system.

Some people have wondered whether Djinn could be extended to enumerate all the inhabitants of that type, instead of just one. Well, no. And here is a diagonalization argument to prove it.

First, it makes things much simpler if we cast everything in terms of integers. Types and expressions can both easily be encoded as integers, for example by interpreting their ascii representations as base 256 numbers. I'll use the notation ⟨x⟩ to denote the integer representing the type or expression x.

Even though our expressions now masquerade as integers, we should still be able to evaluate them.

haskell eval :: Int -> Int -> Int spec ⟨f⟩ `eval` ⟨x⟩ == ⟨f x⟩

The above code is the specification for eval, not its implementation. It is an incomplete specification, because we don't care about the behaviour of eval when it is given integers which don't represent expressions (rendering the left-hand side meaningless) or when these expressions are of incompatible types (rendering the right-hand side meaningless). In what follows, eval should always be used implicitly whenever the code appears to be applying an integer to another.

Next, by contradiction, suppose we did have a version of Djinn which enumerated all of the inhabitants of a type.

haskell inhabitants :: Int -> Int -> Int spec if (p :: T) then ∃i:Int. inhabitants ⟨T⟩ i == ⟨p⟩

Instead of returning a list of all the results, inhabitants takes an extra integer i as a second argument and returns the i^th member of its enumeration. If there are less than i members in the enumeration, then we don't care what inhabitants returns.

Again, that's because the specification is incomplete. It is very incomplete. It doesn't even forbid inhabitants from returning expressions with the wrong type in addition to those who do. It only requires inhabitants not to miss any of the expressions which do have the requested type, because that's all I need in order to derive a contradiction. In fact, I only need to find a single type and a single expression of that type which inhabitants misses. The diagonal, for example.

haskell diag :: Int -> Int haskell diag i = 1 + inhabitants ⟨Int -> Int⟩ i i

This time I did not merely give a specification, but an explicit definition.

The function diag has type Int -> Int, so the specification of inhabitants requires that inhabitants ⟨Int -> Int⟩ i == ⟨diag⟩ for some i. Both sides of this equation should evaluate to the same integer, ⟨diag⟩. And thus, the expressions represented by those identical integers should also be the same. In particular, the expressions should behave the same on all inputs, including input i. But on that input, diag made sure to behave differently, by returning a value that is off by one from the left-hand side's value! Thus, inhabitants ⟨Int -> Int⟩ must have missed diag, as needed.

Now that we know that implementing inhabitants correctly is impossible, what's wrong with the following attempt?

haskell inhabitants :: Int -> Int -> Int haskell inhabitants _ p = p

Okay, so it's not a very serious attempt, but it does satisfy the specification. Remember how I said that I didn't need to forbid inhabitants from returning too many expressions? Well here I am, returning all expressions, all the time, regardless of the type requested. How could I miss any?

Let's walk through the argument again. There is some diag function which I'm supposed to miss. The specification requires inhabitants ⟨Int -> Int⟩ i == ⟨diag⟩ for some i. And with this implementation, this happens when i is equal to ⟨diag⟩. At this point, diag is supposed to stab us in the back by adding one!

haskell diag i = 1 + inhabitants ⟨Int -> Int⟩ i i haskell diag ⟨diag⟩ = 1 + inhabitants ⟨Int -> Int⟩ ⟨diag⟩ ⟨diag⟩ haskell diag ⟨diag⟩ = 1 + ⟨diag⟩ `eval` ⟨diag⟩ haskell diag i = 1 + diag i haskell diag i = loop

The foolish diag, however, was stabbed by our infiltrated agents first. It turns out that calling inhabitants ⟨Int -> Int⟩ i caused diag i not to terminate! Adding one to ⊥ has no effect, and diag failed to distinguish its behaviour from inhabitants ⟨Int -> Int⟩ i, avoiding a contradiction.

What this tells us, is that the original argument implicitly assumed that inhabitants only enumerated terminating expressions. In turn, this tells us that the type inhabitation problem implicitly requires inhabitants to terminate. And with hindsight, it's rather obvious than they should. Otherwise, the type inhabitation problem would be trivial: every single type would be inhabited!

haskell fake_inhabitant :: a haskell fake_inhabitant = haskell let witness = fake_inhabitant haskell in witness

And now, I can finally reveal what it is that makes my perpetual motion engine possible: the inhabitants function involved in my discovery enumerates expressions which, syntactically, have the correct type, but whether the enumerated expressions terminate or not is irrelevant to my discovery. The fact that I won't be able to produce useful work out of it doesn't mean it can't also be a nice theoretical device. But maybe I really should have called it a "perpetually slowing-down engine", to avoid confusion.

update: In other news, it is also impossible for Djinn to exist. But it's only impossible for versions of Djinn which cover strong enough type systems, like Haskell's. From this, I can conclude that Djinn covers a useful fragment of Haskell, and you can conclude that I don't use Djinn very often.

Axes of the lambda cube

Can't see the math behind the greek? For reference, here are the appropriate greek letters for each abstraction mechanism introduced in each axis of the lambda cube. For completeness, lambda abstraction is also included on its own, even though it appears in all axes.

Each cell begins with an example type, followed by an example term of that type. Either the term, the type, or both (...or neither!) will feature a new greek abstraction letter, introducing a variable that can be used on the right of the period.

These new symbols extend the syntax of the calculus, in a way that is made precise in the last lines of the cell. Those lines extend the basic grammar using a functional notation which models variable introductions more precisely than a context-free grammar could.

Even though some cells introduce more than one new abstraction symbol, each cell only introduces one new kind of application. The syntax for application is always just juxtaposition; the syntactic types of the juxtaposed constructs should make it clear which application is meant. The last line of each cell extends the grammar to support this new kind of application, with a bold fragment highlighting what makes the axis unique.

function types
(A → B) →
  A → B
λf:(A → B).
  λx:A. f x

(→) : type → type → type
λ : type → (term → term) → term
(•) : term → term → term

dependent types
(Πx:Nat. P x) →
  Πy:Nat. P y
λf:(Πx:Nat. P x).
  λy:Nat. f y

Π : type → (term → type) → type
(•) : type → term → type

polymorphic types
(∀A. Nat → A) →
  ∀B. Nat → B
λf:(∀A. Nat → A).
  ΛB. λy:Nat. f B y

∀ : (type → type) → type
Λ : (type → term) → term
(•) : term → type → term

parametric types
(A → B → (P : * → * → *) A B) →
  A → B → P A B
λf:(A → B → P A B).
  λx:A. λy:B. f a b

(→) : kind → kind → kind
(•) : ∀⟨type⟩:kind. (type → ⟨type⟩) → type → ⟨type⟩

Testing Chrome Overlays

Writing a Firefox extension involves writing a so-called "chrome overlay", which is an xml description of the interface changes you wish to make.

I'm in the process of learning how to write overlays. That means I make mistakes. Lots of them. They're completely normal stepping stones in the process of learning, and I'm totally prepared to spend lots of time doing nothing but mistakes. But while I'm doing this, I'd rather not spend lots of time doing non mistake-related tasks. Non-mistakes reduce the number of mistakes I can do in one day, and thus increase the number of days spent learning.

If, in addition, the non mistake-related task is repetitive and impossible to automate, then I'm likely to get angry. I'm really angry against reinstalling in-progress Firefox extensions right now. Or at least I was, before I found a way to avoid doing it.

My solution is to add two new buttons to my bookmarks toolbar: one for the chrome I want to overlay over, and one which applies my overlay over it. Don't click those links, just look at the URLs to understand the trick, and then only if you're also trying to learn overlays. For everybody else, well... just wait a little bit. The extension I'm working on is going to be really interesting.

...if my attention is not caught by something else before I complete it, that is.

I want to be a knowledge engineer!

The best thing about being a student is that your job is to learn. Except it isn't really a job at all, since I'm the one paying the university, not the other way around.

The sad thing about being a student, is that it cannot last. Once you've done enough learning, you're expected to go out there in the industrial world and use that knowledge. My current plan is to work in the mornings, raising enough money to pay for my classes autonomous learning (I'm a grad student) in the afternoon. I prefer this to filling out grant application forms.

But I've stumbled upon this fiction-sounding job title, "knowledge engineer", which sounds too good to be true. According to that article, a knowledge engineer acts as an intermediate between domain experts and programmers. So the domain expert does the hard job of finding and reading papers and arguing with other experts and performing experiments and keeping up with the latest research. This process apparently turns experts into brains floating in a vat of brains, thereby losing their ability to communicate with the outside world.

Somewhere in this outside world lies a programmer, who is also a domain expert, an expert in program construction. Thus he lives in his own vat, separate from the domain expert's. The programmer vat is equipped with wheels, and it travels from vat to vat trying to simplify the jobs of the other brains. Many of them perform dull and automatable tasks everyday without realizing that a computer could do it for them, freeing them to do more arguing and reading and experimenting. So the programmers offer to write them useful new tools and the experts agree to explain all of the little details which the programmers could need, and the experts blabber on and on and on and the programmers can't take it anymore. I just need to know whether measuring an increased atmospheric pressure leads to predicting a higher or a lower temperature! Who cares about the details of the moving air masses and the process of cloud formation and the reason altitude messes with our measurement?

I do. I mean the knowledge engineer does, I just wish I was a knowledge engineer. When the programmer vat approaches the expert vat, the knowledge engineer's brain jumps from one vat to the other, and begins to ask questions. He does care about the process of cloud formation because he's naturally curious, and maybe it's not going to help with the problem at hand or maybe clouds, pressure and temperature are all intimately linked in some complicated way which the knowledge engineer just can't wait to discover. Then he jumps back into the programmer vat and explains the parts which turned out to matter to the problem at hand, using words which make sense to the programmers, because at the bottom of his heart, he's one of them. The programmer vat is his own travelling home, the one with the cables floating everywhere and the squeaky mouse-like wheels. Domain experts just love the knowledge engineer, because he cares about their stuff, and programmers also love the knowledge engineer, because he talks their language.

Anybody out there who wants to love me?

Rant against beamer's shaky animation support (and solution)

I love LaTeX.

I love it because TeX is a programming language, and the other typesetting products aren't. Other that that, it's a horrible language.

For some reason, I don't follow the "separate presentation from contents" dogma. I guess it must be a bit strange coming from a guy who otherwise strongly advocates separation of concerns in all manners of code, but that's the way it is. Micromanaging the look of my LaTeX creations involves lots of anger against the program's not-quite-perfect sense of aesthetics, a few wasted night, and a handful of life-saving low-level TeX macros. Tonight's fight involved the latter.

beamer is an impressive LaTeX mod for creating slides. The output is a PDF document, so you can only generate a sequence of static slides. No animations, no sound. I mention it in case you expected slide programs to provide these ridiculous toys; me, I'm used to text-only slides and box-based ornaments. That's because I was using LaTeX to create my slides way before I knew about beamer, so I improvised with what I thought was possible. beamer, with its colors and rounded boxes and navigation and gradually uncovered slides, sure showed me how much I underestimated the extent of the possible.

Yet with all of its features, there's one thing I used to be able to do (easily?) with LaTeX alone, and which beamer doesn't offer: uncovering by substitution. By "uncovering by substitution", I mean a slide transition that doesn't just add or highlight the next element, but which actually changes an existing element. You know, like \alt and \temporal do.

...Ok, so \alt and \temporal actually are beamer commands, so I guess the feature is provided after all. But it's implementation is rather shaky. I mean literally, my slides shake when I use these commands. That's because the alternatives are of slightly different lengths, which slightly displaces the remainder of the text, which makes an unpleasing shaking effect if I use several alternatives in quick succession. Again, most people probably aren't bothered by this at all, but I'm the obsessive type who wants the "presentation" part of his presentations to be exactly right.

As you must have guessed by now: here's my version of \alt. It's called \switch, and just like \uncover, it doesn't shake. Furthermore, it's argument is a list of \case<+>{...} clauses which will appear one after the other. Or at the same time, if you use overlapping ranges. That's both more general and more useful than \alt and \temporal, which are limited to two and three non-overlapping ranges, respectively.

And now that the extent of the possible has been increased once again... a new level of time-wasting attention to details can begin.

Designing a mergeable filesystem structure

In my previous post, I have argued that it would be better if filesystems could be merged without human supervision. This could only happen if conflicts were impossible, but with today's filesystems, merge conflicts are actually inevitable! Let's design a filesystem without this flaw.

My study of conflicts has led me to the study of a family of data-structures which I call commutative types. These structures are abstract data types, in the sense that you can only modify them through their public methods. What distinguishes commutative types is the additional restriction that the internal state of the object must not depend on the sequence of operations which have been performed on it so far, but on the set of operations which have been performed. In other words, the order in which the operations are applied must have no impact.

For example, consider an object whose internal state is a single integer. If the only update operation provided were increment() and decrement(), then this object would be commutative. This is because incrementing and then decrementing yields the same result as decrementing first, then incrementing (we're ignoring overflows for now). Similarly, if double() and triple() were the only operations provided, then the object would again be commutative. On the other hand, if the same object allowed both increment() and double(), then that object would not be commutative.

x + 1 − 1 = x − 1 + 1
x × 2 × 3 = x × 3 × 2
(x + 1) × 2 ≠ (x × 2) + 1

Integers are well studied structures for which commutative operations are known, but in order to represent a filesystem, we will need a commutative object with a much more complicated internal state. Let's design one! What are the requirements?

Well, here's an easy one. Suppose we write() a value in a particular file. If we later read() this same file, then we ought to obtain the value we wrote in it. Now, if we read() the file before we write to it, there's no way we're going to read the same value. Does this mean that any filesystem supporting both read() and write() can't be commutative?

...

Yes and no! It was a trick question. Remember, we're only concerned about the internal state of the object here. Since read() doesn't change this state, it actually commutes with anything. In particular, read() commutes with write(). Unfortunately, this still doesn't make the filesystem a commutative object, because write() doesn't commute with itself...

If we write("foo") to a particular file, then write("bar") to it, then the final state definitely isn't going to be the same as if "bar" was written first. So our commutative filesystem can't even have a write() method.

That's a pretty drastic restriction! We could, however, have a write_xor() method. Instead of replacing the file's contents with its argument, write_xor() would bitwise exclusive-or the content of the file with it. This looks weird and useless, but it would actually produce an okay filesystem. You could still write any value you wanted to the file, you would just need to zero-out the file first, by xor-ing the file's contents with itself. Writing a shorter value in this fashion would leave a padding of zeroes at the end, but we could introduce an end-of-file character to alleviate the problem. All in all, I'm not too dissatisfied with this minimalist interface. And it commutes! You will never see a merge conflict again!

...in theory. But in practice, the result of a merge will be an unreadable mess of binary characters, which is even worse than a conflict. I'm not giving up yet, as I've got plenty of other ideas, but let's keep this so-so idea for now. Because there's another challenge to solve: directories!

If the two branches we want to merge both define the same filename, but one as a file and the other as a directory, what should we do? Should one take precedence over the other? That would work, and it would probably commute, but I have a better solution. What if we kept both? With today's filesystems, every directory's got two names: /foo/bar and /foo/bar/. The first form is usually favoured, out of habit more than anything else, I think. Well, let's not let the choices of the past prevent us from picking the choice of the future today. I'll allow /foo/ to contain both a file named bar and a directory named bar/! And my trees will commute at last!!!

Wait, I do sound more crazy than usual when I say it like that.

Rant against merge conflicts (and a solution strategy)

Version control used to be all about versioning. I never used RCS, but I bet the killer command was something like "rcs commit", to create a new version.

Projects soon grew bigger and version control began to be all about collaboration. The killer command was then "cvs checkout", to get the source and begin collaborating.

Then projects grew even more complicated and it was no longer sufficient just to version text, it was now important to version binaries and directories and symlinks and permissions and ancestry. As version control began to resemble filesystems, the magic occurred in commands like "svn add".

More recently, different distributed version control made forking much easier, and the killer command is now "git branch". But the future of version control, I believe, lies in the one command which never worked quite right: "git merge".

Because of merge conflicts, merging is the only version control command which requires human supervision. Removing this constraint would allow other programs to perform merges, a seemingly small advantage which, in the long run, could actually lead to some very useful and unexpected applications... I'm thinking about unionfs extensions, but there could be many others. Never underestimate the creativity of a million strangers!

I happen to be somewhat of an expert on conflicts, or at least I wish I was. For my master's thesis, I'm currently tackling weaving conflicts in aspect-oriented applications. My conclusion so far is that conflicts are inevitable, unless we work with very restricted structures which are guaranteed to merge properly. I'm trying to find suitably-restricted structures which would be expressive enough to program with.

I think that weaving and merging are very closely related operations. The first attempts to combine code, while the second attempts to combine filesystems. In both cases, unfortunately, the parts to be combined could turn out to be utterly incompatible. Current aspect-oriented languages tend to proceed with weaving anyway, postponing the disaster until runtime. Current version control systems take the opposite approach, refusing to merge until the user has fixed all of the conflicts. But I think it should be the other way around! Incorrect programs ought to fail as early as possible, possibly during the compilation or weaving phase. And for scripting purposes, as I've mentioned, I'd rather have merging succeed all the time.

For my aspects-related research, I've found several restricted structures which combine fine all the time, but filesystems can't be among them. Thus if we do insist on combining filesystems, I claim that conflicts are inevitable. That's why I don't insist on combining filesystems. In fact, you might remember how a few months back, I wished for a framework customizing the relationship between the git repository and the filesystem. This is precisely what I'm arguing for once again! Let's use one of my magic restricted structures inside the repository, so that merges succeed all the time. Then if users want to use the repository to track their filesystem, their logs, their cats, or whatever, let them write a translation between the repository and the thing they want to track. Now that would be doing one thing and doing it right, rather than letting filesystem concerns creep into the repository's code base.

What do you think? I am being more crazy than usual?

Rant against choices (and solution)

This is a mashup between Barry Schwartz's paradox of choice talk and sigfpe's presentation of ordinals as a survival game.

Apparently, math tells us that there are three kinds of totally ordered single player games.

• ∅, where we've got no choices at all. if society gives you this choice, blame society.
• successor ordinals such as 42 or ω + 1, where you've got many choices, including one which is obviously better. if society gives you this choice, pick the best move and smile.
• limit ordinals such as &omega, where no matter which choice you make, you could have made a better one. if society gives you this choice, pick as best as you can, then blame yourself for not choosing better.

Barry Schwartz noticed that consumerism yields societies with lots of choices of the third kind, which makes people unhappy. Perhaps his book offers practical solutions, but in his talk he just seemed nostalgic of the days when society gave him choices of the second, perhaps even of the first type. Well, I've got a message of hope for him.

If ordinals are any indication of the evolution of society (!), then we're going to experience an alternation of successor and limit situations, so we're going to be fine half of the time. Society is not going to revert to the old days of the finite ordinals, when there were few enough choices to make correct decisions. Instead, I predict that we're going to have even more choices, but that this time it's going to be pretty obvious which one to make. ω + 1: one step above the competition. Would make a great slogan. Soon after, said competition is going to adopt the new technology and we'll reach ω + ω, another disappointing limit ordinal. Then a new technology will project us into ω + ω + 1, and the first few consumers will experience satisfaction once again.

In short, the secret to happiness is not to have low expectations, as Barry suggests, but to be an early adopter!

Google's badware hoop (and solution)

As you've probably noticed, Google began warning users against some websites, making them read through a "this site may harm your computer" message before allowing them to proceed. I'm glad to see you care about me, Google, thanks, but no thanks. I can take care of myself.

The problem is, you can't turn this off.

Until today, of course, since I'm publishing this greasemonkey script. There are other scripts like this here and there, but I obviously prefer mine better. My version highlights dangerous links in red, letting you into the site without asking you to jump into any hoop. In addition, a second link allows you to check Google's diagnostic page, which explains how the hell they could be led to believe that my local tree-hugging eco center switched from wanting to recycle my computer to wanting to harm it.

filenamed

Does your shell script use temporary files? Does it clean up the temporaries after it dies? What if the user aborts your script early by using ^C? What if he feels mean and uses kill -9 instead?

Not using temporary files is the easiest way out of this mess, but unfortunately there are situations where this is unavoidable. Let's say, for example, that you want to diff the output of two programs. Using temporary filenames, this can be done as follows.

bash progA > outA.tmp bash progB > outB.tmp bash diff outA.tmp outB.tmp | progC bash rm outA.tmp bash rm outB.tmp

It's possible to use pipes to eliminate outA.tmp

bash progB > outB.tmp bash progA | diff - outB.tmp | progC bash rm outB.tmp

It's also possible to eliminate outB.tmp

bash progA > outA.tmp bash progB | diff outA.tmp - | progC bash rm outA.tmp

But with this technique it isn't possible to eliminate both temporaries at once. To see why this is is a problem, consider the case where progB is stuck in an infinite loop. In that case, the user is justified to kill your script using the magic CTRL-C combination; and even if the action isn't totally justified, the user can do whatever he wants and it's your job to keep your program from fooling up even when the user does. In any case, ^C will kill both progB and your script, which won't have the opportunity to delete its temporary file. It's not a very critical flaw, but I'd feel better if the script was robust enough to withstand this.

A naive solution could be to disable ^C.

bash trap "" SIGINT bash progA > outA.tmp bash progB > outB.tmp bash diff outA.tmp outB.tmp | progC bash rm outA.tmp bash rm outB.tmp

But this will only annoy the user, who will just kill your script using kill -9 instead of ^C. And you can't disable kill -9. So what would be a better solution?

The solution I've been advocating until today is as follows.

bash trap "rm -f outA.tmp outB.tmp" EXIT bash progA > outA.tmp bash progB > outB.tmp bash diff outA.tmp outB.tmp | progC

This will erase the temporaries on exit, whether the exit is normal or due to ^C. It still doesn't work against kill -9, but what does?

Well, I'll tell you what does. If user-mode code can't clean up on SIGKILL (the signal which -9 selects), then we'll use kernel-mode code. Incidentally, the kernel already contains code to clean up unclosed file descriptors, and we can use this to our advantage.

When we used "-" as an argument for diff, it really was just a short name for /proc/self/fd/0 (that is, standard input). This path names a virtual file which is deleted by the kernel when grep terminates. These virtual files correspond to file descriptors, so if we can create additional file descriptors, then we can create auto-cleaning temporary files.

read_fd3.rb fd3, fd4 = IO.pipe read_fd3.rb fd3.getc # wait until fd4 is opened by an outside process read_fd3.rb fd4.close read_fd3.rb exec(*ARGV) write_fd3.rb $stdout.close write_fd3.rb $stdout = File.new "/proc/#{ARGV.shift}/fd/4", 'w' write_fd3.rb $stdout.write 'x' write_fd3.rb $stdout.flush write_fd3.rb exec(*ARGV) bash ( bash progA | ruby read_fd3.rb diff /proc/self/fd/0 /proc/self/fd/3 & bash ruby write_fd3.rb $! progB bash wait $! bash ) | progC

The first ruby program creates two linked descriptors and leaves them open, letting the exec'd program use them. In this case, the exec'd program is diff, and it is told to compare /proc/self/fd/0 against /proc/self/fd/3. The first is just standard input, which comes from progA. The second is one of the linked file descriptors which were left open.

The second ruby program writes to the other linked file descriptor. This effectively sends the output of progB to the virtual file which diff is reading, as needed.

write_fd3.rb also writes an additional byte before the transfering the control to progB. This byte is needed because the end-of-file only occurs once all programs have closed all of their handles on the virtual file. read_fd3.rb has one of those handles, but it cannot close it until write_fd3.rb has secured its own handle, or the end-of-file will come too soon. So write_fd3.rb sends one byte to tell read_fd3.rb that it is now safe to close its handle.

You'll notice that this virtual file strategy is a bit awkward to use. And now that you have learned how to do it by hand, I can reveal you a secret: this strategy was built into bash all along! The syntax is as follows.

bash diff <(progA) <(progB) | progC

Concise, isn't it? However, this isn't the end of the story. There are some programs, unfortunately, which look at their input multiple times. You can't do that. Closing /proc/self/fd/3 is just as irreversible as closing stdin! And you can't use fseek(), either. So sorry, virtual files freed by the kernel. I tried to make this work, I really did, but... you're ordered, I'm random. We're just not made for each other.

Here's a more flexible solution. If the dying process cannot cleanup, then another process should take care of it. Preferably, a process which always runs, a daemon process. Whose job is to allocate and delete temporary files. A given client would reveal its process-id to the daemon, which will allocate a file for the client and delete it once the process with the given process-id has disappeared from the system. It could have disappeared for different reasons, including normal termination, ^C, and even kill -9.

If you think implementing a daemon would be going through a lot of trouble just for a few temporary files, then you'll be happy to hear that I've already went through this trouble for you. I called my daemon filenamed, and the corresponding client, filename, can be used as follows.

bash diff $(progA | filename) $(filename $(progB)) | progC

I also provide a wrapper called "<", which can be used as a drop-in replacement for the bash syntax <(...) which I introduced earlier. My version, of course, allows fseek().

bash diff $(\< progA) $(\< progB) | progC

There are a few aspects of my daemon which I'm not that proud of, but which I don't intend to fix. First, it depends on ruby, even though it's use is not ruby-specific. I'm just too lazy to reimplement it in C. Second, it's not very secure. Clients shouldn't be able to take control of the daemon, but they could easily request it to keep files until process 1 dies, that is, forever. Clients shouldn't be able to modify the files of other clients, but they could easily read them.

If you can live with that, enjoy!

Rant against .gitkeep (and solution)

Git claims to be miles ahead of Subversion, looking down on it as "only" fixing CVS's flaws. Well, one annoying CVS flaw is its failure to archive the existence of directories on the server side, and it seems that git is still behind Subversion in this respect.

Of course, it would be incorrect to state that CVS doesn't track directories at all. It tracks changes to individual files, where a "file" is really a path from the root CVS checkout. On the server side, a CVS archive is simply a working copy where each file is replaced by a "<file>,v" version, archiving diffs in RCS format. So each RCS file on the server side is located in a directory which corresponds to a directory in the working copy.

In addition to the text-based changes which current diff formats convey, RCS can also distinguish between an empty file and a deleted file. It would have been really simple to use a "<dir>,v" file to distinguish between empty and deleted directories, but for some reason, CVS didn't. And it's really annoying.

When you check out a CVS project, the client will create all the directories it knows of, including the ones which were once needed a long time ago to store some obsolete file in the project. To avoid polluting your working copy in this manner, the CVS client offers a "-P" option, which skips the creation of directories whose files are deleted. But this is annoying too (albeit less so), since this will skip the "bin" directory and the build process will fail. Assuming you weren't foolish enough to archive your binaries into CVS, that is.

The standard fix is to archive a "bin/.keepme" file whose sole purpose is to exist whenever "bin" is supposed to exist. It's very similar to the "<dir>,v" idea I suggested above, except that it's called "<dir>/.keepme,v", and that it's visible to users. So it's still annoying, but vanishingly so.

The Subversion team decided that they could get rid of the last few specks of annoyingness in the obvious way, by keeping track of the directory proper.

The git team decided to stick with the CVS way of doing things. They even have an FAQ advising to add the ".keepme" files (which they call ".gitignore").

Anyway, I wrote these wrapper scripts to hide those ".keepme" files from the users. I name them ".gitkeep", and they're still slightly visible in that you have to create and add them manually, but once you commit them, they're gone. And my version of git-status reminds you to add them, instead of pretending that it added everything when in fact it ignored empty directories.

Rant against Firefox version checks (and solution)

I'm not particularly fond of Firefox's XUL+js architecture, but I'm more than willing to live with this unusual choice if it allows people to easily write Firefox extensions to customize their experience.

But did you ever notice that most of the plugins break every time you update Firefox? I thought that APIs which change this fast must reflect a development model where refactoring is frequent. I'm glad when teams decide that code quality is more important that backward compatibility, but my enthusiasm doesn't seem to be widely shared.

As a side-note, I think that the developers of the Linux kernel have found a great way to please everyone. They maintain backward compatibility for their external interface, the system calls which all Linux applications use, while allowing themselves to refactor their internal interface at will. This is unfortunately not enough since drivers depend on this internal interface, just like Firefox plugins depend on the browser's internal XUL interface. But instead of requiring driver developers to update their code at every release, the kernel team encourages driver developers to commit their code to the kernel tree and to let the kernel developers update the drivers themselves.

Today, I've upgraded Firefox from version 3 beta 5 to version 3 RC1, and as usual it broke many of my plugins. Now, the shocking part is that there isn't supposed to be any change at all between those two versions! So if the internal API didn't change... Could it be that the plugins were broken by something bogus?

What happened is that Firefox's extension mechanism requires each plugin to specify a range of versions on which it is supposed to work, and they're not supposed to pretend that they work on versions which haven't been released yet. What a bad idea! This means that every single Firefox release will break every single plugin except those that cheat and pretend to know the future. This in turn means that every single plugin needs a maintainer to diligently follow Firefox's release schedule and to bump the range of his plugin every time. How boring! I'd rather have those people working on new extensions.

So in case your favorite plugin's maintainer is too bored to do this, here's how to do it yourself.

First, find the install.rdf file associated with your plugin:

bash grep 'em:name' ~/.mozilla/firefox/*.default/extensions/*/install.rdf output ~/.mozilla/firefox/5edzcuns.default/extensions/{e4a8a97b-f2ed-450b-b12d-ee082ba24781}/install.rdf: em:name="Greasemonkey"

Inside the file, just increase the value of em:maxVersion to your current Firefox version, or to some absurdly large version number if you're bold enough not to fear the future.

Gmail's fullscreen mode (and solution)

Gmail has a so-called "fullscreen mode" which ought to please me: it dedicates all of the browser's screen real estate to the message I'm reading. No pesky sidebars at all. Ain't it great? Well, it turns out I'm rather difficult to please.

What should I do once I'm done with the message? I will either want to delete it, to archive it, or to read my next message. But I can't do any of those in fullscreen mode! How come there's no button to come back to my inbox?

Okay, so this is a trivial problem with a trivial solution: just bookmark Gmail's inbox and be done with it! But of course, I wouldn't be telling you about this if I had settled for the trivial solution.

Here is my solution: widest gmail. It's a bookmarklet, so don't bother clicking on it now, it won't lead you anywhere. But if you put it in your toolbar, and click it once you're in Gmail's conversation mode, it will toggle the fullscreen mode on and off.

Rant against sidebars (and solution)

I don't browse fullscreen.

Let me repeat that, in case it isn't absolutely clear. My internet browser is never maximized. I have a few windows sprinkled about my screen, the more the merrier, until I run out of space to put them. Thanks to you, web designers (but do continue reading even if you're not a web designer as I have a goodie for you at the end), this occurs as soon as I launch firefox.

But it's not your fault. I know how deeply you care about your audience. I know you are worried about the resolution of your website, that's why you gather statistics about our screen resolutions before exclaiming: "thank god nobody runs at 640x480 anymore, but I still need to cater to those poor saps who are still stuck with 800x600". So you build a website spanning those entire 800 pixels and I need to maximize my browser to see it and I get unhappy and I double my resolution, possibly buying a new screen to accommodate the change. And now your statistics tell you that even less people are stuck at 800x600 and you build an even wider website and I buy an even wider screen and I want to slap you silly for misunderstanding my contribution to your statistics.

Your assumption that your audience is browsing fullscreen is wrong. But assume for a moment that you realized your awful mistake and began measuring the size of the browser window instead of measuring the resolution of the screen. Then your statistics would still confirm that browsers are usually larger than what your site needs, and you will still greedily increase its size. This is because I came to your website looking for a piece of information, which I will continue to desire despite the size of your website. Your statistics will report the sizes at which your audience was reluctantly browsing your site, not the sizes at which they would prefer to browse it.

Now suppose that, in your infinite kindness, you decided to redesign your site so that it would scale automatically to fit each viewer's browser size. Would this make me happy at last? I would have hoped so, but most websites today do scale to fit my browser's size, and I'm still not happy.

The source of my annoyance is sidebars. Their width is usually small and fixed, leaving the bulk of the space to the actual contents. The problem here is that "small" is measured according to the web designer's standards, and the web designer is browsing fullscreen on a very large screen. This means that in my browser, those annoying sidebars will take up two thirds of the space and the contents will be so squished that I will need to resize my browser despite the website's struggling efforts to accommodate my size choices. At least when the websites had a fixed width I could scroll those sidebars out of the way.

Anyway, Gmail uses two sidebars, and I wrote a script to get rid of the right-hand one. That's the "goodie", "solution", constructive part of this rant.

The sidebar I'm removing contains mostly text ads, but that's not the reason I'm removing it. In fact, if you came here looking for a way to remove those adds, I'd advise you not to. Well, sure, go ahead and remove the ads if they bother you, but if the sidebar doesn't bother you as well then don't get rid of an entire bar just to get rid of a few ads. The sidebar does contain a few useful things; I've never used its "New window", "Print all", nor "Expand all" buttons, but the bar does occasionally contain golden suggestions. It once parsed the text of the message I was reading, discovered that it was an invitation, and provided me with a button to add the event to my calendar. It even got the time, place, and event description right! I bet that Google will find more cool ways to understand our messages and provide us with smart buttons, but I'll miss out on them if I remove this sidebar. Oh well, I guess my hatred is greater than my enthusiasm.

Here is the script: wider gmail. It's a bookmarklet, so don't bother clicking on it now, it won't lead you anywhere. But if you put it in your toolbar, and click it once you're in Gmail's conversation mode, it will toggle the right-hand sidebar on and off. And if you'd rather have the bar hiden by default, here is a Greasemonkey script which should do the trick.

Gmail signature bookmarklet

update: As of November 2008, gmail now has a setting to place your signature above the quotation if you want to. Thanks Google!

---

When you reply to a message, Gmail creates a text editor with your cursor at the top, a giant quotation containing the message you're replying to, some useless double-colon separator, and your signature.

Gmail's default cursor location encourages top-posting, which I don't really mind. The problem is that the signature is bottom-bosted, so people tend to write a second signature above the giant quotation. A few wasted characters, not a big deal.

The real problem is that I know that Gmail has stuffed my signature down there at the very bottom, so I'm moving it back up every single time I reply to an email. Were I in Vim, this would be just another few wasted characters ("GD``p"), but I'm not and I grew annoyed. So I automated it.

Here it is: uppersig. It's a bookmarklet, so don't bother clicking on it now, it won't lead you anywhere. But if you put in in your toolbar, and click it immediately after hitting "reply", it will move the signature and refocus the editor.

Ok, so having to click a button everytime I reply to an email is also annoying, which is why I used to have a Greasemonkey script to do this automatically, but Gmail's dynamic javascript code is making this difficult.

edit: by the way, Google often changes internal Gmail details which break my script, but I fix it everytime, so just bookmark a fresh copy if you ever find that my bookmarklet stopped working. Last updated 2008-09-19.

Of comonads and nightclubs

In this awesome explanation of monads, you have been building space stations under the master directive that all stations must output their astronauts in space suits. We're going to build nightclubs. In winter. Under the master directive that clients must take off their wintercoats before dancing.

We are especially concerned about the entrance procedure. There is a sequence of things which clients need to perform before they are allowed in. Maybe it's a private nightclub and you need to authenticate yourself. Maybe it's a high profile nightclub and you need to leave your limo keys to the valet. Maybe it's a paranoid nightclub and you need to be inspected for weapons. At one place I've been if you arrive early enough, they give you two empty glasses when you enter, and during the course of the night you can order exactly two free drinks. Maybe it's a rave and you need to buy enough drugs to scare sleep away for the entire night. Maybe there's a cover fee, and maybe it's lady's night so a girl's entrance procedure will be different from a guy's. And most importantly, you need to check your wintercoat at the coat check.

Now imagine you are working for a nightclub entrepreneur who had so much success so far that he plans to build a whole slew of different kinds of nightclubs. In consequence of his first success, he considers himself an expert of dancing floor design; he won't let you play near those. Nightclub entrances, on the other hand, they're all yours.

At the Entrance Parts Supermarket, you discover that entrances are made out of modular parts. There is a cover fee part, a parking part (valet not included), and even a case of part which can distinguish between guys and girls. There are pre-assembled kits, for common combinations such as a counter for both the cover fee and the coat check.

Your boss doesn't really understand the point of modular design. He insists that he will only pay for parts which make sure that clients check out their wintercoats. No amount of argumentation will convince him that a single nightclub entrance will only ever need a single coat check module, and that it's okay for the other modules not to repeat the same job. So you end up buying a bunch of reusable entrance parts which you can't even compose since once free of their wintercoats, clients won't be able to go through further wintercoat-removing steps.

Okay, so what did you do in the spacesuit example when you ended up with a whole bunch of incompatible space stations? You built a bind robot to extract the astronaut out of his spacesuit, feeding the astronaut into the next space station. Our bind robot will do exactly the opposite: in so far as a spacesuit can be thought of as a really expansive and overkill wintercoat, our bind robot (=>>) will put a client back into a suit, feeding the suited client into the next entrance part.

This system allows us to use any ordinary modular entrance part, provided it is available as a pre-assembled kit with a coat check included. It also allows us to use those fancy new parts which don't need to be grafted with coat checks, because taking clients out of their coats is part of their raison d'être. For instance, crooked nightclubs might want to use the all-in-one cover fee + coat check counter not as a pre-assembled kit, but as a simple coat check counter with crooks hired to steal any valuables from the coats. A nightclub featuring a lady's night might want to avoid the embarrassment of having to ask a "borderline" client what his/her gender is. Because of the (ridiculous) convention of placing a coat's zipper handle on one side for girl coats and on the other side for guys, a special coat check counter could provide a heuristic. At a beach-themed nightclub, clients could be required to put on swimwear, and it would make sense to provide lockers for clients to store both their street clothes and their wintercoats.

Monads were kinds of spaces, and different monads required different kinds of spacesuits with different procedures for astronauts to take them on and off. Some special space stations had a built-in ability to put astronauts into suits. A monad-specific robot named "bind" allowed ordinary and special space stations to intermingle. That was the whole point of monads: a framework to elegantly integrate special functions with the rest of our computation.

Comonads are kinds of snow, and different comonads require different kinds of wintercoats with different procedures for clients to take them on and off. Some special entrance parts have a built-in ability to take clients out of their wintercoats. A comonad-specific robot named "bind" allows ordinary and special entrance parts to intermingle. That is the whole point of comonads: a framework to elegantly integrate special functions with the rest of our computation.

Both monads and comonads are needed because they handle different categories of special functions. And bimonads, actually called arrows, can handle either kind, as well as brand new special functions which no monad nor comonad has ever dreamt of...