Quantifiers, metaprogramming and concepts

1. Intro

Quantification expresses the extent to which a  predicate is true over a set of elements. Two forms are the most common:

  • Universal \forall
  • Existential \exists

To define the quantifiers, let A represent an expression, and let x represent a variable. Then:

  • Universal Quantification: If we want to indicate that A is true for all possible values of x, we write “\forall\ x\; A\;“. Here \forall\ x\; is called the universal quantifier, and A\; is called the scope of the quantifier. The symbol \forall is pronounced “for all“.
  • Existential quantification: If we want to indicate that A is true for at least one value of x, we write “\exists\ x\; A\;“. This statement is pronounced “There exists an x such that A“. Here \exists\ x\; is called the existential quantifier, and A is called the scope of the existential quantifier.

We elaborate on the topic as follows: In section 2 we describe quantification in the template metaprogramming context, in section 3 we explore related standard library facilities introduced in C++17 and section 4 adds concepts to the equation. Finally, in section 5 we draw some concluding remarks.

2. Use in metaprogramming 

Metaprograms often use predicate logic in creative ways. For example, type queries in generic code are used to constrain, dispatch, specialize, activate or deactivate code at compile time. Even until C++14, expressing predicate logic at compile time was cumbersome, when handling variadic arguments, involving a helper type and crafty use of boolean logic:

The C++17 Standard allows for much simpler (almost mathematical) syntax, by folding over the logical operators:

Above we define two variable templates that become true or false depending on the value of their (boolean) template arguments. Since they’re conceptually and syntactically simpler, as well as cheaper in terms of instantiations, we’ll prefer these to built subsequent tools.

Making the Quantifiers

To define our quantifiers we need to involve the predicates, essentially the process that produces the list of boolean we feed to the above variable templates. Let P be a predicate over a type and Ts a type list, then:

These quantifiers could be used for example to check that a list of types is trivially copyable:

A toy example can be found here . Of course the quantifiers can be used inline w/o stub code like the are_tc variable template above.

Generalized Predicates – Currying metafunctions

A limitation of the code so far is that it can only be used for univariate predicates. Say we had a predicate that needed 2 or more variables to compute, how would we handle it? Here the is_smaller type checks that the size of its operands is ascending:

You might argue that “ \forall T\; \in\; A\; smaller\;” i.e. is_smaller holds for every type T in typelist A, has no meaning and you’d be right (smaller than what?). Thankfully we need to introduce a restriction which is that multivariate predicates are to be bound until only one argument position is free and we can do that either in place (by loading the needed types throughout our interfaces) or by introducing a compile time bind, essentially currying metafunctions:

With this in place here’s how to verify that a type is smaller than every type in a typelist:

3. The Standard library

The universal and existential quantifiers are defined in the C++17 Standard library as conjunction and disjunction respectively. Their main difference from what we defined so far is that they short-circuit in the expression level, i.e. not every expression needs to be well-formed if the result can be computed before their evaluation. This comes in handy in certain cases, but it implies they’ll have to be recursively implemented (I’m pretty sure the following implementation is attributed to Johnathan Wakely):

i.e. we stop inheriting when the expression has computed. In contrast, our flattened instantiations implementation excels in compile times and instantiation depth violations. Choose wisely between flat and short circuiting depending on your use case.

As an example, recursive instantiations here use an integer sequence of 18 elements to break a tuple, essentially due to its move constructor. The move constructor has a conditional noexcept that is implemented recursively. Therefore, for each template argument, a constant number of additional instantiations is required (the implementation e.g. of is_nothrow_move_constructible in terms of is_nothrow_constructible which is implemented in terms of __is_nt_constructible and so on, for 15 instantiation levels!). This means that each template argument for tuple requires 15 additional instantiation levels for this check. On top of that, 9 levels are always required (constant depth). Therefore, 17 arguments require an instantiation depth of 17*15+9 == 264 (default for clang 3.7 was 256).

Another example use of this mechanism would be to elaborate on quantification the other way around, i.e. one type vs many predicates (instead of 1 predicate vs many types we’be doing so far):

4. Concepts

Concepts are predicates. And as such a simple extension of our quantifiers can encapsulate concepts as well:

To get an idea of how this could be used check below:

or this Demo (disclaimer: only to showcase the use of quantifiers with concepts, don’t try to find particular meaning in the code).

5. Conclusions

Metaprogramming is changing. For the better. Better techniques and more expressive syntax are emerging that will allow library writers to produce more elegant code. Users of this code will have a better experience due to more comprehensive compiler errors. The price we have to pay is understanding the formalities and theory involved with this ecosystem; the bet to be won is Stroustrup’s “make simple things simple” claim, so that modern C++ can be “expert friendly” but not “expert only”.

6. References

On Quantifiers and predicate logic

Standard library documentation

Related Stack Overflow articles listed chronologically

Related code on the blog’s repository


Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s