You Are More Than a Coder



The answer — by demonstration — would take care of that, too.

 — Isaac Asimov, [The Last Question][last-question]


From time to time, I stumble across something beautiful and true. It happened recently, and this is me trying to share it. It has a formal name, the [Curry-Howard correspondence][chc], but it’s one of those rare bits of knowledge that, once known, feel so inevitable, they almost don’t need a name. It may not impress you as deeply as it did me; you may not see the point; you may not care. But it is the most profound and elegant thing I know about programming.

• • • • •

Programming is an act of creation. Constrained by business needs, by hardware limitations, by our own reach which may exceed our grasp, we are still, in the end, creators. But — we are not artists. There is elegance in what we do; it is not the goal. There can be beauty in the product; it is subordinate to function. There can even be transcendence; it is not a given. We have obligations: stability, reliability, functionality, effectiveness, productivity, testability, maintainability; we have jobs, and if art results, fantastic; if it doesn’t, that’s fine.

Neither are we engineers or scientists. We don’t design physical objects; we don’t care about gravity, electricity, or magnetism; evolutions is irrelevant to us; neuroscience is a mystery. We create in an abstract world that interacts, in points, with the concrete, but that is separate from it. We manipulate ideas; we transform data; we process knowledge; we present concepts. Under it all, no matter how we dress things up, what we do is invent new ways to move around zeros and ones. There’s a name for our kind: we are mathematicians.

Some of us may not think so. Some of us hated mathematics in school, some ran from calculus, some balked at statistics. Some of us came to programming through an altogether different route, via the liberal or fine arts. Some of us may even be bad mathematicians. But mathematicians we all are. That is what the Curry-Howard correspondence tells us.

• • • • •

If you’re like me, your first instinct when you look at a function is to wonder what it does. Take the following Ruby method:

def add_numbers(arr)
  arr.reduce { |memo, num|
    memo + num
  }
end

What it does is clear: it adds ([or concatenates…][types-as-units]) the values in an array. But let’s look at it a different way; let’s look at only the declaration: def add_numbers(arr). Even by itself, it carries information: it says there is a method that takes an object as a parameter and returns another object.1

Let’s look at a similar method in Swift:

func addNumbers(arr:[Int]) -> Int {
    return reduce(arr, 0) { memo, num in
        return memo + num
    }
}

What does the declaration tell us this time? It tells us hat there is a function that takes an Array of Ints and returns an Int. Obviously this declaration conveys more information than the Ruby one; that’s an important point and I’ll get back to it later. For now, let’s just recognize that in both languages, declarations contain information.

I’m still phrasing the information in terms of what the function or method does. It’s equally appropriate to phrase it as a statement about the world:

  1. The Ruby method declaration states that there exists a way to transform an object into a (possibly different) object.
  2. The Swift function declaration states that there exists a way to transform an Array of Ints into a single Int.

Once you start making statements about the world, though, you have to back them up. Doing so in this case is easy: write at an implementation. How do you show that there is a way to transform an object into another object? Write code that does it! How do you show there is a way to transform an array of integers into a single integer? Write code that does it! And how do you know your implementation is valid? You type-check it.

And this is the important caveat. A proof of a declaration is valid if it type-checks. But that doesn’t mandate a particular implementation. Here is a Ruby method that type-checks,2 i.e. that matches its declaration:

def add_numbers(arr)
  return nil
end

This implementation doesn’t do what the function name says, but that doesn’t prevent it from type-cheking. Likewise, this Swift implementation function fulfills its declaration, despite not adding the numbers either:

func addNumbers(arr:[Int]) -> Int {
    return 0
}

From this, we can get to the essence of the Curry-Howard correspondence, which is that type systems define a logic: a set of statements that can be made and proven using only types. Function declarations are the statements; implementations are the proof. Since the name of a function isn’t part of its type, it places no constraints on the proof; that’s why we can have a Swift function named addNumbers that does no such thing. What we can’t do is declare our addNumbers function as above, but have it return a String. Its type doesn’t allow it.

Put all this another way, every time we write a function declaration, we state a theorem, and every time we write an implementation that type-checks, we prove it. As I said, we are all mathematicians.

• • • • •

If type systems define the statements that can be made and proven, that would imply that different type systems let you prove different things. And indeed, that is the case. Some type systems are powerful and others are not, in a very precise sense. Ruby’s type system is not very powerful, because not many statements can be made with it. In fact, only one statement can be made. Here it is:

Every group of objects can be transformed into an object.

To be a little more charitable, there is in fact an infinity of statements that can be made, but they all follow the same pattern:

This is a fundamental limitation of the language — but notice that it doesn’t make the language any less useful for software development. It’s simply that its type system isn’t very expressive.

Swift, by contrast, is much more expressive. Here are a few statements that can be made with Swift function declarations:

As before, we need to remember that statements being more specific is not the same as their admitting only one implementation (in other words, a unique proof). However, an expressive type system serves to narrow down the possible implementations to only those that satisfy the statements’ type, and an automated type checker serves to verify that the type declarations are respected — that is, proven.

And this is where we come full circle to how this knowledge is changing the way I program. Because while the Curry-Howard correspondence shows that there is a direct mapping between doing something and proving that it can be done, there is a world of difference in how I approach a task and how I approach a proof.

In the past, my mental process when I wrote a function has been:

  1. What does my function need to do?
  2. What parameters does it need to do it?
  3. Implement it.

I am now shifting to a different way of thinking:

  1. What truth do I know about the world?
  2. Prove it.

The first two questions are condensed into one, because the parameters are the first part of any theorem: given X, Y is true. By tying them at the hip, I find that I often have to think about whether the statement makes sense before starting to write code, particularly if I try to write in a [referentially transparent][rt] style.

The action item, though, is where the main difference lies. An implementation has to work; a proof must be ironclad. While the type checker will verify that my implementation proves the function declaration, I am invariably trying to prove a much more specific statement than can be expressed in a declaration. For instance, I would not be trying to prove just that a touch and a map can be transformed into a coordinate; I would be trying to prove that they can be transformed into the coordinate of the point on the map where the touch occurred. This is not expressible in the function declaration, but it is still a provable fact about the world. I find that thinking about my functions as proofs makes me write better code, code that is more cognizant of edge cases and error conditions.

This approach is completely language-agnostic and type-system agnostic. Yes, stronger type systems allow the function declaration to be more specific. Since all strong type systems typically include a type checker in the compiler toolchain, a side-benefit is that they also verify the declaration’s proof is valid.3 But once again, valid is not necessarily useful. I’m trying to encourage a different way of thinking about what it means to program, not pushing a particular language or type system.

• • • • •

I’ve tried to keep this post light on the theory of the Curry-Howard correspondence, because what was revelatory to me wasn’t the mathematics of it, but rather the idea that I could approach programming as an exercise in proving theorems. For actual details, I highly recommend Alyssa Carter’s [fantastic introduction][type-systems-and-logic] to the formalism of type systems and the logics they correspond to; it’s an incredible read and I learned a lot from it — with a grin on my face the whole time. This stuff is just cool.

If you’re not so inclined, though, I still hope you have gotten something out of this rumination. If nothing else this: that you, the programmer, are a mathematician. Every time you’ve written a function declaration, you have had something to prove. And proven it you have, over and over again.








1 In Ruby, every scope has a return value, and it is the last value computed in the scope. Therefore, every function has a return value, whether return is explicitly called or not. In addition, everything in Ruby is an object (including entities other languages might treat as primitives, like nil).↩︎


2 Ruby does have types; they’re just so simple that a Ruby method is consistent with its declaration by virtue of being syntactically correct.↩︎


3 And as [increasingly powerful type systems][idris] start appearing, more and more of the proof will be verifiable.↩︎

[last-question]: http://www.multivax.com/last_question.html
[types-as-units]: http://nomothetis.svbtle.com/types-as-units
[chc]: http://en.wikipedia.org/wiki/Curry–Howard_correspondence
[type-systems-and-logic]: https://codewords.hackerschool.com/issues/one/type-systems-and-logic
[rt]:http://en.wikipedia.org/wiki/Referential_transparency_(computer_science)
[idris]:http://www.idris-lang.org

 
89
Kudos
 
89
Kudos

Now read this

Smashing Swift

I have been playing with [Swift][] ever since Apple announced it at this year’s WWDC. I was lucky enough to be there, and I spent a good chunk of my time in the labs, coding and asking the engineers who created it questions. There is... Continue →