Lambda the Ultimate

Three properties that I aim for in my language design are commutativity (ability to rearrange expressions within a group), associativity (ability to regroup expressions), and idempotence (ability to duplicate or eliminate expressions that are sitting next to one another) all without changing a program's meaning. These three properties, taken together, give a programming language a very declarative feel. Basically, you can treat each expression as an independent 'declaration' of program behavior, while still allowing parametric abstraction for groups of declarations. Commutativity means there is no implicit control-flow in the syntax (i.e. sequencing in code != sequencing in behavior). Associativity makes it easy to rearrange and abstract common subgroups of declarations. Idempotence makes it easy to introduce duplicate expressions to help with refactoring, and later to eliminate duplicate expressions to help with performance.

One can control many properties by tying them to algebraic structure. For example, the object capability security model 'works' by tightly associating connectivity with the algebra. You get some useful algebraic rules for who can talk to whom and the flow of 'side-effects'. Ocap model isn't perfect - most implementations allow for covert channels (based on resource consumption and load) - but it helps enough to simplify reasoning.

A very useful algebraic property is algebraic closure. To clarify: the common meaning of 'closure' in programming is the capture of lexical environment in a first-class function or new object, but the algebraic meaning of 'closure' is that the composition is the same sort of thing as the whole. Basically, algebraic closure is what makes a programming model compositional.

Surprisingly, very few models of programming are truly compositional. Too many fail to achieve algebraic closure for critical functional or non-functional properties. Actors model is not compositional because individual actors have different concurrency properties than a group of actors. Programs using mutexes are not compositional because the composition of programs can deadlock even if both subprograms are individually safe. Remote procedure calls are not compositional because a sequence of calls has very different performance characteristics than creating one huge call (thus we end up needing scripts or batching). Concrete class-typed OO is not compositional because it is difficult to present a group of objects as a single object.

For easy, robust, scalable composition, a programming model must take into account all the important properties (both functional and non-functional) and ensure algebraic closure and control over those properties. That includes concurrency and synchronization, latency and efficiency, partial-failure handling and recovery, communication and side-effects. Failure to achieve algebraic closure forces programmers to be much more aware of the implementation details of the elements being composed (i.e. imagine having different rules for adding numbers based on prime factors) and hurts abstraction because developers must write code specialized for the components. A requirement to grok implementation details of components limits the practical scalability of the model (due to limited capacity of programmers).

A single language may support or model many programming models. Doing so can be costly - in terms of complexity - if it means violating algebraic closure (whether within a model or at the boundaries between them). If there is an objective definition for simplicity and elegance, it is 'algebraic closure'.

If I were to point out a few of the more 'composable' programming models, they'd be: pure functions (esp. total functions - guaranteed termination), functional reactive programming, concurrent constraint programming, logic programming (esp. simplified forms such as Datalog, Dedalus, Bloom), synchronous reactive programming, and concatenative languages such as Forth. A duck-typed OO model obeying ocap principles would also be up there (E language, Newspeak).

Beyond a single programming model, one can also compare and grok models using algebraic concepts.

Finding a homomorphism with equivalent behavior proves that one language is at least equal in power to another, and can help you understand a model. Finding two homomorphisms, one in each direction, means the languages have identical power. Finding an isomorphism (two homomorphisms whose composition is the identity function) indicates a tight relationship between models, such that one can be used easily to verify the other. Finding a homeomorphism between models is essentially a declaration of expressive and compositional equivalence - i.e. a homeomorphism is an isomorphism where a small local change in model A has a corresponding small local change in model B. I tend to distinguish programming models based on the notion of homeomorphism.

I've not read Algebra of Programming so I cannot recommend the book one way or the other, but I've found that one eye on algebraic properties and morphisms is essential for effective programming language design, and helps me understand and learn from existing models.

Proving the equivalence of expressions is at the heart of [correct] program optimization. By using transformations that preserve the meaning (FSVO, e.g. extensional identity) of expressions, we can try to find better (e.g. that are simpler or that use less space or time to compute) programs that we know are are equivalent. So, while it doesn't always tell us *how* to transform programs to get better ones, the approach lets us know that whatever transformation we apply is correct.

In practice, most of the examples in Algebra of Programming seem trivial, in that you could have figured the final program (and even the correctness proof for some) out without going through Squiggol... that's the programmer's equivalent of solving a system of equations by trial and error. The formalism introduced in that book is useful because it gives us tools to approach program optimization in a more systematic manner, leaving more human creativity, time and energy for other tasks.

The first half of the book is basically just the beta/eta rules of the lambda calculus, which as you note is familiar enough to be unexciting.

It's the second half, where they move to sets and relations, which is much more interesting. Lots of optimization problems can be specified in generate-and-test terms (ie, find the best solution out of this set of possible solutions), and the equational reasoning used to derive good solutions is quite pretty -- I really liked their derivation of the TeX line-breaking algorithm.