Algebra

Don't you just hate those Microsoft developers?*

You've just started replacing that fusty old, string-based SQL Builder with a modern, class-based model, featuring fully composable queries, query clauses, and expressions, all the way down to basic arithmetic. Suddenly, they bring out LINQ.

Some time later, recognising the monadic algebra behind the new pattern-based query comprehension keywords, you decide to harness it to implement the continuation monad, which will allow you to write asynchronous code in a purely synchronous paradigm. Suddenly, they announce async/await.

No matter how good, how revolutionary your design, the fact remains that you just can't beat a good keyword. There's simply no better or more powerful implementation, nothing tidier than a well conceived and designed primary language feature. This observation highlights the need to know thoroughly, completely and perfectly, the nature of the feature under implementation.

Unless your main business is writing compilers, your greatest enemy is the client specification, perhaps represented by the design engineer, stating non-goals like there is no requirement to compare or subtract two fields. Because you know that there will be. And when that requirement is finally unearthed, you will already have been forced down the Agile pipe, and have implemented a horribly hobbled subset of the operations that would have been required to express properly a well-formed algebra - of queries, or asynchronous tasks, or whatever.

The sad truth is that many of us lack the basic mathematical skills to appreciate the seachange wrought on your design by a proper, complete, closed and proven algebra. And while the scope for such effort and expenditure by application developers continues to shrink, and a good job too, with the increasing power and usability of production compilers and other tools; still it is imperative to be ready to identify such situations when they do occur, and to be prepared to design the solution along veins of sound, algebraic principles.

Vindication

Eric Lippert's latest blog article is a beautiful exercise in such pure, abstract, algebraic thinking, and brilliantly displays its payoff. He asks, what in C# is a type? The naive answers most of us would propose, these have all by now been discounted with the aid of counterexamples, in the predecessor article. A type is not a name with a set of values. Neither can it be defined as a set of assignment rules. Still less is a type some kind of predicate for determining which among an infinite set of values belong to it. Eric demonstrates the strictly formal application of mathematical logic at work in his conception, when he actually makes essential use of Russell's Paradox in proving the inadequacy of these attempts!

A type, in the mind of compiler writer Eric, is nothing more than an abstract mathematical entity obeying certain algebraic rules. He follows this definition with a good analogy based on Giuseppe Peano's axiomatic definition of natural number. Turning back to his equally axiomatic type definition, he then shows how its axioms can be used to construct compile-time proofs of runtime type safety (ignoring temporarily wrinkles like the cast operator, or unsafe array covariance).

But perhaps the best illustration of the power of the abstract analytical approach is seen when he dips into Gödel's undecidability results, and identifies areas where such proofs cannot be constructed reliably. The lesson here is that still, the formal analysis rigorously controls the progress toward a compiler solution; this time accurately and unambiguously delineating the "holes in the road" where practical workarounds must be applied, or where - in measurably unrealistic, and perfectly predictable situations - a compiler failure can be tolerated.

Expression too complex to analyse.

Pic: Giuseppe Peano, from Wikipedia. Not actually a Microsoft dev.
*I just love those Microsoft developers!