The Spherical Cow in Vacuum, Part 1 - Lambda Calculus

There is an old joke about a farmer who figured out that egghead boffins who can split an atom could surely figure out a way to get his cows to produce more milk.  So he contacted the physics department in the famous university and sweet-talked them into agreeing to consider his problem. The intrepid team of scientists eagerly took on the challenge and spent countless hours arguing, writing equations on chalk boards, and publishing papers. Days passed, then months, and then the team announced the break-through - they made huge progress!  When the farmer heard about it, he promptly inquired so as to what the solution is and how can he make use of it at his farm.  "Not so fast..." replied boffins "Our solution only applies to spherical cows in vacuum."

As the joke goes, it's only partially a joke.  One of the pitfalls of doing science is that you could build a nice theory which seems to fit your problem quite well... all the simple problems have solutions, but when you get to interesting ones, it all breaks down.  Pesky details ignored by the theory suddenly become major issues, and the nice theoretical framework now gets in the way of finding a right way of thinking about the problem at hand.

The most fundamental mathematical theory to the practical computing is lambda calculus (often written as "λ-calculus").   It was created in 1930 by Alonzo Church as part of his life-long work on foundations of mathematical logic (specifically, he came up with it in order to show that Entscheidungsproblem is not solvable).  It has an enormous influence on computer science and programming practice, from the first programming languages of late 1950s, and all the way to the contemporary fad of functional programming (which can be described as a thin veneer of syntactic sugar on top of λ-calculus).  It is beautiful, and some expressions have even gained cult status among the cognoscentes (see Y combinator).

It is also the biggest spherical cow in vacuum one could find. Let me explain.

The central concept of λ-calculus is abstraction (denoted by letter λ).  It is easily recognizable in a notion of subroutine in pretty much every general-purpose programming language. The abstraction contains the body (a formula) it wraps, and bound named variable(s) used in the formula and exposed by the abstraction as arguments (in programming parlance this would be formal parameter(s) of the subroutine).

Specific values of parameters can be applied to an abstraction, using an operation called β-reduction which basically replaces every mention of a bound variable (parameter) with the formula of the specific value.  (There are some other details - such as dealing with renaming of variables to avoid name conflicts, these are not important for the purpose of this discussion).

These λ-calculus operations of abstraction and application are directly reproduced in pretty much every conventional programming language and serve as the primary mechanism for abstraction (which corresponds to a subroutine declaration) and abstraction unwrapping (I deliberately use non-standard term here to avoid more specific connotations) - which corresponds to either subroutine call or subroutine code in-lining (the semantics is the same, but these choices offer different trade-offs between executable code size and performance).  For brevity, I'll omit closures - they are just syntactic sugar over plain old calling of subroutines by pointers.

In  λ-calculus, expressions have no side effects and are pure:  they only produce result value when evaluated,  and that value will be the same when all variable values are the same.  And this is here where the nice theoretical construct starts to clash with the reality.

Execution of any computer code has side effects.  Let it sink.

Some of these side effects are intrinsic: they change the state of the computer in ways directly accessible to the program (functional programming style attempts to minimize these), but more interesting side effects are extrinsic: the time it takes to run the code, the amount of heat generated by the computation, data being stored in and evicted from cache, network packets being sent, changes in pixel luminosity on displays, etc, etc.   Because programs run strictly within confines of CPU and RAM - which are not directly accessible from outside, a program without extrinsic side effects would be a null operation.  The sole purpose of running programs on computers is to generate extrinsic side effects.

The problem is: λ-calculus (and operations of subroutine declaration and calling in programming languages) do not admit existence of side effects.  It is not possible to describe side effects or do anything about them within this formalism.  (Of course,  λ-calculus is Turing-complete and so any kind of non-interactive program can be converted into it - but this is a ridiculously low bar for fitness for any practical purpose, as anybody who ever tried to write a slightly non-trivial program for Turing machine or played with Church numerals surely knows.)

From the point of view of programming ideal abstract machines there is no difference, for example, between bubble sort and quicksort.  They are equivalent.  On real computers, of course, there's a world of difference.

There's another name for the side effects which are not formally representable in the language: abstraction leaks.  And they are the root of the problem with modern software development, as we discussed in the previous post.

So here we have it: by using a seemingly perfect theoretical concept to represent abstraction and abstraction unwrapping in our programming languages we got ourselves into the corner - because that particular theoretical concept does not fit the reality of computation using physical computers. Part of this is confusion between mathematical and engineering abstraction, part of it is inertia and lack of reflection on the basic tenets of the discipline.

We obviously need to find a way to represent side effects (both intrinsic and extrinsic) within a programming language if we ever going to overcome the abstraction level ceiling. Prof. Gregor Kiczales offered an outline of a design attempting to do just that in his 1992 article, but no practical implementation or design proposal ever came out of it.

The question is what the right mathematical structure and corresponding practical representation for the engineering abstraction would be?  Stay tuned.  We're not done with sacred spherical bovines yet (see Part 2).