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
• Existential

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 ““. Here is called the universal quantifier, and is called the scope of the quantifier. The symbol is pronounced “for all“.

• Existential quantification: If we want to indicate that A is true for at least one value of x, we write ““. This statement is pronounced “There exists an x such that A“. Here 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:

	template< bool… Bs >
	using bool_sequence = std::integer_sequence< bool, Bs… >;
	template< bool… Bs >
	using bool_and = std::is_same<
	bool_sequence<Bs… >, bool_sequence<(Bs || true)… >>;
	template< bool… Bs >
	using bool_or = std::integral_constant< bool, !bool_and< !Bs… >::value >;

view raw

old_ct_predicate_logic.cpp

hosted with ❤ by GitHub

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

	template <bool… Bs> constexpr bool all_v = (… && Bs);
	template <bool… Bs> constexpr bool any_v = (… || Bs);

view raw

new_pred_logic.cpp

hosted with ❤ by GitHub

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:

	// ———————————— "is there ?"
	template <template <class> class P, class… Ts>
	constexpr bool existential_quantifier = any_v<P<Ts>::value…>;
	// —————————————– "are all ?"
	template <template <class> class P, class… Ts>
	constexpr bool universal_quantifier = all_v<P<Ts>::value…>;

view raw

quantifiers.cpp

hosted with ❤ by GitHub

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

	template <class… Ts>
	constexpr bool are_tc = universal_quantifier<std::is_trivially_copyable, Ts…>;

view raw

univ_quant_example.cpp

hosted with ❤ by GitHub

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:

	template <class T1, class T2>
	using is_smaller = std::integral_constant<bool, sizeof(T1) < sizeof(T2)>;

view raw

is_smaller.cpp

hosted with ❤ by GitHub

You might argue that “” 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:

	template <template <class…> class C, class…Ts>
	struct curry
	{
	template <class T>
	using type = C<Ts…, T>;
	};

view raw

meta_curry.cpp

hosted with ❤ by GitHub

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

	struct S0 {};
	struct alignas(2) S1 {};
	struct alignas(4) S2 {};
	struct alignas(8) S3 {};
	int main()
	{
	static_assert(universal_quantifier<curry<is_smaller, S0>::type, S1, S2, S3>);
	}

view raw

meta_bind_example.cpp

hosted with ❤ by GitHub

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):

	template<class…> struct conjunction : std::true_type { };
	template<class B1> struct conjunction<B1> : B1 { };
	template<class B1, class… Bn>
	struct conjunction<B1, Bn…>
	: std::conditional_t<bool(B1::value), conjunction<Bn…>, B1> {};
	template<class…> struct disjunction : std::false_type { };
	template<class B1> struct disjunction<B1> : B1 { };
	template<class B1, class… Bn>
	struct disjunction<B1, Bn…>
	: std::conditional_t<bool(B1::value), B1, disjunction<Bn…>> { };

view raw

con_dis.cpp

hosted with ❤ by GitHub

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):

	template <class T, template <class> class… Ps>
	constexpr bool satisfies_all_v = std::conjunction<Ps<T>…>::value;
	template <class T, template <class> class… Ps>
	constexpr bool satisfies_any_v = std::disjunction<Ps<T>…>::value;

view raw

quantify_variadic_predicates.cpp

hosted with ❤ by GitHub

4. Concepts

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

	// ———————————————————–
	// ——————– to express "1 predicate Vs many types"
	template <template <class> class P, class… Ts>
	concept bool existential_quantifier = any_v<P<Ts>::value…>;
	template <template <class> class P, class… Ts>
	concept bool universal_quantifier = all_v<P<Ts>::value…>;
	// ———————————————————–
	// ———————————————————–
	// ——————– to express "1 type Vs many predicates"
	template <class T, template <class> class… Ps>
	concept bool satisfies_all = all_v<Ps<T>…>;
	template <class T, template <class> class… Ps>
	concept bool satisfies_any = any_v<Ps<T>…>::value;
	// ———————————————————–

view raw

concepts_n_quantifiers.cpp

hosted with ❤ by GitHub

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

	template<typename T> concept bool Data = requires(T t) { t.data; };
	template<Data… Ts>
	requires existential_quantifier<std::is_move_constructible, Ts…>
	auto f(Ts… ts)
	{
	std::cout << "version for data\n";
	return 0;
	}

view raw

quant_concepts_example.cpp

hosted with ❤ by GitHub

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

• Quantifier (Wikipedia)
• Predicate logic (tutorials point)

Standard library documentation

• conjunction
• disjunction

Related Stack Overflow articles listed chronologically

• Implementing variadic type traits
• Type trait to check that all types in a parameter pack are copy-constructible
• Check a parameter pack for all of type T
• How to combine conditions from type_traits the standard way

Related code on the blog’s repository

• predicate_logic.h
• predicate_logic.cpp