C++ 中的 Concept：把代数证明交还给编译器

题外话，提到鸭子类型，就很难不想到 C++ 的 concept。作为一种强静态类型语言，C++ 的类型系统长期以来都可以被理解为一种集合建模：声明一个类的字段，是在声明集合中元素的构成，实际上近似于给出一个元组；声明函数、方法和重载运算符，则是在定义作用于这些集合之上的算子。古典时代区分过程与函数，但我个人认为，过程本质上也是在程序状态，或某个局部状态之上作映射，所以不强行区分反倒相当合理。甚至说，它还不是多重集建模：在 C++ 的对象模型中，不同的完整对象通常必须能够由地址加以区分；空对象也至少占一个字节。趣事是，早年我看到用 private 继承实现 has-a 关系时，总觉得这属于绕路的矫饰，后来才知道空基类优化（EBO）的意义：省下那一个字节，进而避免一串对齐赤字，确实很香。C++ 极具辨识度的模板机制，在 static reflection、类型推导、编译期运算等神乎其技的用法之前，其本意毕竟是泛型；而泛型在更抽象的层面上，就是从一类过程里抽取代数过程。这就要求程序员自行检查：自己所定义的集合，是否满足该过程所需的代数性质。那套显学说，写代码，尤其是等待编译通过的时候，其实是在完成一种构造性证明；好比你必须证明某个集合满足域公理，才有资格调用域的性质。古早时期，也就是 concept 之前，维护代数结构的责任主要交给程序员的心智；编译器则近乎冷酷地实例化、推导，然后在失败时吐出不可读的模板天书。如今有了 concept，本质上是在向编译器提供代数结构的信息：编译器可以先在定义层面自动证明或证伪相关命题，这对人的认知负荷是一种极大的释放。许多手法，比如 restrict 一类扩展性限定、volatile 关键字和 attributes 这类语言特性，实际上也都是在向编译器补充信息，使局面不至于继续滑向不可控；所谓语义约束，说到底就是在改写信息的边界。