Specify axioms for concepts

Reason

A meaningful/useful concept has a semantic meaning. Expressing these semantics in an informal, semi-formal, or formal way makes the concept comprehensible to readers and the effort to express it can catch conceptual errors. Specifying semantics is a powerful design tool.

Example

template<typename T>
    // The operators +, -, *, and / for a number are assumed to follow the usual mathematical rules
    // axiom(T a, T b) { a + b == b + a; a - a == 0; a * (b + c) == a * b + a * c; /*...*/ }
    concept Number = requires(T a, T b) {
        { a + b } -> convertible_to<T>;
        { a - b } -> convertible_to<T>;
        { a * b } -> convertible_to<T>;
        { a / b } -> convertible_to<T>;
    };

Note

This is an axiom in the mathematical sense: something that can be assumed without proof. In general, axioms are not provable, and when they are the proof is often beyond the capability of a compiler. An axiom might not be general, but the template writer can assume that it holds for all inputs actually used (similar to a precondition).

Note

In this context axioms are Boolean expressions. See the Palo Alto TR for examples. Currently, C++ does not support axioms (even the ISO Concepts TS), so we have to make do with comments for a longish while. Once language support is available, the // in front of the axiom can be removed

Note

The GSL concepts have well-defined semantics; see the Palo Alto TR and the Ranges TS.

Exception

Early versions of a new "concept" still under development will often just define simple sets of constraints without a well-specified semantics. Finding good semantics can take effort and time. An incomplete set of constraints can still be very useful:

// balancer for a generic binary tree
template<typename Node> concept Balancer = requires(Node* p) {
    add_fixup(p);
    touch(p);
    detach(p);
};

So a Balancer must supply at least these operations on a tree Node, but we are not yet ready to specify detailed semantics because a new kind of balanced tree might require more operations and the precise general semantics for all nodes is hard to pin down in the early stages of design.

A "concept" that is incomplete or without a well-specified semantics can still be useful. For example, it allows for some checking during initial experimentation. However, it should not be assumed to be stable. Each new use case might require such an incomplete concept to be improved.

Enforcement

Look for the word "axiom" in concept definition comments

View on isocpp.github.io →

template<typename T> // The operators +, -, *, and / for a number are assumed to follow the usual mathematical rules // axiom(T a, T b) { a + b == b + a; a - a == 0; a * (b + c) == a * b + a * c; /*...*/ } concept Number = requires(T a, T b) { { a + b } -> convertible_to<T>; { a - b } -> convertible_to<T>; { a * b } -> convertible_to<T>; { a / b } -> convertible_to<T>; };