Concepts in C++: Returning Algebraic Proofs to the Compiler

As an aside, once duck typing comes up, it is hard not to think of concept in C++. As a strongly statically typed language, C++ has long allowed its type system to be understood as a kind of set-theoretic modeling: declaring the fields of a class is declaring the constitution of elements in a set, approximately the specification of a tuple; declaring functions, methods, and overloaded operators is defining operators over those sets. Classical terminology distinguishes procedures from functions, but in my view a procedure is, in essence, also a mapping over program state, or over some local fragment of state, so refusing to draw a hard boundary is quite reasonable. One might even say that this is not multiset modeling either: in the C++ object model, distinct complete objects must generally remain distinguishable by address, and even an empty object occupies at least one byte. A small anecdote: when I first saw private inheritance used to implement a has-a relationship, I thought it was needless ornamentation taking the long way around; only later did I understand the point of empty base optimization (EBO): saving that one byte, and thereby avoiding a cascade of alignment deficits, is indeed rather delicious. C++‘s highly distinctive template mechanism, before all the sorcery of static reflection, type deduction, compile-time computation, and related techniques, was after all intended for generic programming; at a more abstract level, generic programming is the extraction of algebraic processes from a class of procedures. That, in turn, requires the programmer to check whether the set they have defined satisfies the algebraic properties required by the process. A certain fashionable doctrine says that writing code, especially waiting for compilation to succeed, is in fact a form of constructive proof: just as one must prove that a given set satisfies the field axioms before one is entitled to use the properties of a field. In the ancient period, which is to say before concept, the responsibility for maintaining algebraic structure was largely assigned to the programmer’s mind; the compiler, meanwhile, instantiated and deduced with an almost cold indifference, and when it failed, emitted unreadable template scripture. Now that concept exists, what it really does is provide the compiler with information about algebraic structure: the compiler can first prove or refute the relevant propositions at the level of definition, which is an enormous release of cognitive load. Many techniques, such as extension-style qualifiers like restrict, the volatile keyword, and language features like attributes, are likewise ways of supplying the compiler with additional information, keeping the situation from sliding further into the uncontrollable. A semantic constraint, in the end, is nothing other than a rewriting of the boundary of information.