The Universe of Discourse

Thu, 20 Jun 2019

Sufficiently advanced software

A couple of days ago my sleepy brain mashed up Clarke's Law:

Any sufficiently advanced technology is indistinguishable from magic.

and Hanlon's Razor:

Never attribute to malice what can be explained by stupidity.

to produce these words of wisdom:

Any sufficiently advanced software is indistinguishable from malice.

(Why yes, I had spent the evening dealing with Git. Why do you ask?)

This sounded like something Bryan Horstmann-Allen would have said, so with his permission, I am naming it after him.

BDHA's Law? BDHA's Razor? No!

Dated '80s graphic featuring neon-lit brushed-metal letters that

[Other articles in category /misc] permanent link

Mon, 17 Jun 2019

Don't let the man page write checks that the programmer can't cash

My big work project is called “Greenlight”. It's a Git branch merging service. After you've pushed a remote branch, say mjd.fix-bugs, you use a very thin client program to ask the Greenlight server to land your branch on master and publish it for you:

    greenlight submit mjd.fix-bugs

Greenlight analyzes the branch to see if it touches any sensitive code that requires signoffs. If so it contacts the correct people on Slack, and asks them to review it. Once they have approved it, Greenlight rebases the branch onto the current master and pushes the result back to master. If the push fails, it retries silently. Throughout, it communicates via Slack what is going on.

A user, Locksher, complained last week that it didn't do what he had expected. He had a Git pre-push hook he had written. Whenever he ran git push, his pre-push hook would look to see if he was pushing to master. If so, it would look at the messages of the commits he was trying to push. If any of them contained WIP or !fixup or !squash, it would abort the push.

With Greenlight, this check wasn't done, because Locksher never pushed to master himself. Instead he pushed to some topic branch, and then asked Greenlight to publish it to master, which it did, including his WIP commits. Oops!

Locksher asked if it was possible to have Greenlight “respect local hooks”. Once I understood what he wanted, my first suggestion was that he wrap the greenlight client in a shell script that did the check he wanted. My second suggestion, less work for him but also less immediate, was that the Greenlight client could look in .git/hooks for a greenlight-pre-submit hook, and run that before communicating with the server, aborting the request if the hook failed. I think this would adequately solve the problem, especially if the calling convention for the new hook was identical to that of pre-push. Then you would just:

        ln -s pre-push .git/hooks/greenlight-pre-submit

and get exactly the desired behavior. I said that if Locksher wanted to implement this, I would include it in the standard client, or alternatively I would open a ticket to implement it myself, eventually.

Locksher suggested instead that the greenlight client configuration should support this:

    respect-git-hooks = true

I didn't have time then to answer in detail, so I just said:

I consider that very unlikely.

Here's what I said to him once I did have time to answer in detail:

  1. There are currently 23 documented Git hooks, and it's not immediately clear what it would mean to “respect” many of them. I'd have to go over the man page and decide, for each one, what the behavior should be, then possibly implement it, and then document it. Just to pick one example, should Greenlight “respect” your prepare-commit-message hook? If so, how?

  2. Even for the hooks where the correct behavior seemed clear to me, it might seem clearly something else to someone else. So the feature is severely under-specified and seems likely to cause confusion. I foresee a future of inquiries like “I set respect-git-hooks but Greenlight didn't run my pre-auto-gc hook.”

  3. It is an open-ended promise. The way the option is phrased, it guarantees to “respect” every hook. So it commits me to keep track of what new hooks are introduced in every future version of Git, and to decide what to do about each of them.

  4. Since greenlight runs on your local machine, the local version of Git may vary. What if the behavior of Git's pre-cake-slicing hook changes between Git 1.24 and Git 1.26? Now Greenlight will have to implement two behaviors, and look at your local Git version to decide what to do.

Oh, and 5, it is a YAGNI.

In contrast, the functionality provided by greenlight-pre-submit is something someone has actually asked for. It is small, sharply bounded in scope and its definition is completely under my control.

I will elaborate a little on the main items 1–2, that different people might have different ideas about what it means to “respect” a local hook. Consider Locksher's specific request, for greenlight to “respect” his pre-push hook. Another user, say Zubi, could object, quite reasonably, that greenlight submit is not the same as git push, and that the correct way for it to “respect” her pre-push hook is to ignore it. “I want my pre-push hook run when I push a branch,” she might say, “not when I do greenlight submit.” Who could argue with that? (Other than Locksher, of course.)

So then I would have to add an escape hatch for Zubi, so that everyone who didn't want Locksher's feature would have to affirmatively opt out of it.


[Other articles in category /prog] permanent link

Sat, 08 Jun 2019

The inside-outness of category theory

I have pondered category theory periodically for the past 35 years, but not often enough to really stay comfortable with it. Today I was pondering again. I wanted to prove that !!1×A \cong A!! and I was having trouble. I eventually realized my difficulty: my brain had slipped out of category theory mode so that the theorem I was trying to prove did not even make sense.

In most of mathematics, !!1\times A!! would denote some specific entity and we would then show that that entity had a certain property. For example, in set theory we might define !!1\times A!! to be some set, say the set of all Kuratowski pairs !!\langle \varnothing, a\rangle!! where !!a\in A!!:

$$ 1×A =_{\text{def}} \{ z : \exists a\in A : z = \{\{\varnothing\}, \{\varnothing, a\}\} \} $$

and then we would explicitly construct a bijection !!f:A\leftrightarrow 1×A!!:

$$ f(a) = \{\{\varnothing\}, \{\varnothing, a\}\}$$

In category theory, this is not what we do. Everything is less concrete. !!\times!! looks like an operator, one that takes two objects and yields a third. It is not. !!1\times A!! does not denote any particular entity with any particular construction. (Nor does !!1!!, for that matter.) Instead, it denotes an unspecified entity, which happens to have a certain universal property, perhaps just one of many such entities with that property, and there is no canonical representative of the class. It's a mistake to think of it as a single thing, and it's also a mistake to ask the question the way I did ask it. You can't show that !!1×A!! has any specific property, because it's not a specific thing. All you can do is show that anything with the one required universal property must also have the other property. We should rephrase the question like this:

Let !!1×A!! be a product of !!1!! and !!A!!. Then !!1×A\cong A!!.

Maybe a better phrasing is:

Let !!1×A!! be some object that is a product of !!1!! and !!A!!. Then !!1×A\cong A!!.

The notation is still misleading, because it looks like !!1×A!! denotes the result of some operation, and it isn't. We can do a little better:

Let !!B!! be a product of !!1!! and !!A!!. Then !!B\cong A!!.

That it, that's the real theorem. It seems at first to be more difficult — where do we start? But it's actually easier! Because now it's enough to simply prove that !!A!! itself is a product of !!1!! and !!A!!, which is easily done: its projection morphisms are evidently !!! !! and !!{\text{id}}_A!!. And by a previous theorem that all products are isomorphic, any other product, such as !!B!!, must be isomorphic to this one, which is !!A!! itself.

(We can similarly imagine that any theorem that mentions !!1!! is preceded by the phrase “Let !!1!! be some terminal object.”)

[Other articles in category /math] permanent link

Fri, 07 Jun 2019

Disco ball technology

A little while ago I wrote:

I think a disco ball would not be out of place at Versailles.

I just remembered that good mirror technology is perhaps too recent for disco balls to have been at Versailles. Hmmm. Early mirrors were made of polished metal or even stone, clearly unsuitable. Back-silvering of glass wasn't invented until the mid-19th century.

Still, a disco ball is a very forgiving application of mirrors. For a looking-glass you want a large, smooth, flat mirror with no color distortion. For a disco ball you don't need any of those things. Large sheets of flat glass were unavailable before the invention of float glass at the end of the 19th century, but for a disco ball you don't need plate glass, just little shards, leftovers even.

The 17th century could produce mirrors by gluing metal foil to the back of a piece of glass, so I wonder why they didn't. They wouldn't have been able to spotlight it, but they certainly could have hung it under an orbiculum. Was there a technological limitation, or did nobody happen to think of it?

[Other articles in category /tech] permanent link