Equality is a (useless) transmutation machine

Even since I heard about the Curry-Howard isomorphism, I've been wondering: to which computational principle corresponds equality? and the axiom of choice? and all those other mathematical concepts which would probably be much more intuitive to me in computational form? Unfortunately, there is no Curry-Howard dictionary translating concepts from one domain to the other, much like a French-English dictionary would translate words from one language to the other.

A few of the correspondances are well-known. A proposition corresponds to a type, and the proofs of this proposition correspond to the inhabitants of this type. A theorem using the hypothesis A to prove proposition B corresponds to a function from type A to type B.

A number N corresponds to a type with exactly N inhabitants. The multiplication A × B corresponds to the tuple type (A, B). The addition A + B corresponds to the algebraic type Either A B, whose set of inhabitants is the disjoint union of the inhabitants of A and the inhabitants of B. The exponentiation B^A corresponds to the function type A → B. But what is equality?

In Agda, a programming language / theorem prover exploiting the Curry-Howard isomorphism, (propositional) equality is defined as follows.

agda data _≡_ {X} : X → X → Set where agda refl : (x : X) → x ≡ x

I must admit that this doesn't help much. This states that the only valid proof for x ≡ y is refl x, and even then, it only proves that x ≡ x. In other words, the only inhabitants of the type x ≡ y are values of the form refl x, which actually have type x ≡ x.

A more inspiring piece of Agda code is an example showing how to make use of an equality proof.

agda subst : {X : Set} agda → (P : X → Set) agda → (x y : X) agda → x ≡ y agda → P x agda → P y agda subst P .v .v (refl v) p = p

This code takes some arbitrary proposition P(x), say, "x is prime", a proof that x equals y, a proof that P(x) is true, and concludes that P(y) is also true. For example since 7 is prime and 3 + 4 equals 7, it follows that 3 + 4 is also prime. The code does this by pattern-matching on the proof that x ≡ y, obtaining refl v for some value v. Since refl v has both type v ≡ v and type x ≡ y, Agda concludes that x and y are both v. This changes the type of p from P x to P v and the type of the goal from P y to P v, making it possible for subst to return p.

The feat is more impressive if we use counter-factual equalities. If P(x) says that "x is pink", and you have a proof that Leonardo the Flamingo is pink, and also a counter-factual proof that Leonardo the flamingo is "equal" to Bob the Filthy Frog, then you can convince anyone that Bob is pink, thereby gaining him access to all those cool pink-only bars in town. An x ≡ y equality instance is like a machine you can use to transmute x's access cards into access cards for y.

For this reason, it is in the interest of all the cool pink kids that equality instances should be hard to forge.

And equality instance really are hard to forge. refl x has type x ≡ x, remember? The only transmuter you can build is the one which doesn't actually perform any transmutation. Hence my title: equality is a (useless) transmutation machine.

Oh! One last thing. The bird's-eye view of this post is that equality is a transmutation machine because by using subst, equality instances can be used to transmute things. Couldn't it be that using functions other than subst, equality instances could be used to do even more incredible (yet useless) things?

It turns out the answer is no: an equality instance is no stronger than a substitution machine. The proof of this is that from a substituting machine, we can obtain an equality instance, as follows.

agda unsubst : {X : Set} agda → (x y : X) agda → (subst : (P : X → Set) → P x → P y) agda → x ≡ y agda unsubst x y subst = subst (λ – → x ≡ –) (refl x)

We simply use our substitution machine to transmute the trivial equality instance refl x of type x ≡ x into an equality instance of type x ≡ y. Tada! Equality is (as strong as) a transmutation machine.

How to cope with changing requirements

the context

Programming an application is a complicated endeavor. Often, people outside of the field greatly misjudge the amount of work necessary to implement one; either by vastly underestimating the work necessary to build programs similar to the ones they already use, or by vastly overestimating the work necessary to build programs unlike the ones they already use.

A misguided client in the first category might, for example, come to you saying he would like you to build him a program "just like Microsoft Word, except that [such and such]". An equally misguided client in the second category might be manually adding the same country code to a list of phone numbers every day, because his partners are sending him phone numbers of potential clients, he has to post these phone numbers on a website in order to filter out the numbers that are on the do-not-call-list, and the website expects the phone numbers in a slightly different format.

In a way, the second situation is sadder than the first. In the first situation, the programmer will of course explain immediately that Microsoft Word has a lot of hidden features and that single-handedly duplicating the entire application would take forever. But in the second situation, the poor client might continue to manually perform the task for years until a colleague with some programming experience happens to step into his office at the right moment to ask what he's doing.

the problem

This lack of magnitude appreciation causes a lot of problems when comes the time to settle for the price of a commissioned application. Ideally, clients would know exactly what they want and programmers would know exactly how much work it will take to build what is wanted. In practice, however, clients change their requirements mid-way once they see how their imagined program looks like in real life, or ask for "just one little extra feature" which requires a complete redesign of the application. Programmers could simply stubbornly refuse to deviate from the specification; but alas, not only this isn't a way to treat a paying client, programmers are also notoriously bad at estimating the amount of time a given task will take them.

There exists a number of methodologies (agile, SCRUM...) which aim to solve this problem by involving the client in the process. The basic idea is very simple: if you show intermediate versions of the product to your client, he will change his mind sooner, so you will waste less time working on a version which your client doesn't like.

I must admit that I am not very familiar with these methodologies. My understanding is that they are intended for teams of programmers working together on a single project, so that you would only bother to learn about a methodology if your manager suggests or decides that your team should use it. For an individual programmer working with an individual client, these methodologies look overkill. They sell books explaining these methodologies, and you want to write code, not read books.

the solution

Here's a very simple, no-book-required methodology.

The first time your client comes to see you, let him awkwardly attempt to explain what he wants. Ignore his ill-conceived notion of what the program should look like or how one would use it; you broadly understand what he's trying to accomplish, right? Good. Now, give your client a magazine and tell him that the first version of his software will be ready in an hour. "ONE hour? no way." He'll be shocked, but he'll wait. He won't even notice that you haven't started discussing compensation yet. I bet he didn't expect to see a demo for at least a month.

Now, of course you won't have a working program ready within an hour. But you certainly have the time to create a crude mockup of a program. A few buttons here and there, with the keywords you have heard him rant about written on them. They don't have to do anything when you click on them. The important thing is to have something to show the client as soon as you can.

Once the hour is complete, show the program to the client and tell him that this is version zero, and that many features are still missing. Okay, let's be honest, all of the features are missing, but from the point of view of the client, what you are showing him is already impressive. It's an application built just for him, with buttons labelled with the things he cares about, and it's only been an hour since he met you. I bet he thinks that making the buttons actually do something is "just one little extra feature".

And actually, it is. Let your client play with the mockup interface for a while, then ask him to pick one single feature he would like you to add during the next hour. Help him to pick something of the appropriate complexity. Now, once he understands that the application is going to be built step-by-step, one small feature at a time, and now that he understands how small such a one-step feature actually is, now is the time to discuss pricing.

Ask to be paid a fixed price per version. He's already seen the first version, and you have just told him what the next version will look like, so he can roughly assess how much a single version is worth to him. Negotiate the price as needed. Of course, the client doesn't have to visit every hour for the entire project; after confidence is built, he will probably ask on his own if he could simply give you a list of half a dozen features and come back six versions later. Just make sure not to let him list all the features of his misconceived dream application in one go.

Having the client only pay for running programs also gets rid of one painful situation in which the programmer is making progress on the internals of the application while the client sees an accumulation of bills and no concrete progress, gives up, and decides to cut his losses by abandoning the project. But the point of this payment method is mainly to let the client notice by himself that he can't keep on asking for "just one more little feature" forever, as each time he does so, he pays a little more. Eventually, the client will need to decide that the software is good enough for his needs, and walk away with the last version he paid for.