Free theorems in C++: are templates inherently ignorant and neutral with their objects of unknown types?

Question

Famously in Haskell if we have a function without a concrete type we can deduce something about its behavior, for example

f : a -> a

will always be the identity.

With Java Generics we cannot prove that generic functions have a certain behavior since we can use instanceof or the methods on the Object base class to work around the restrictions, however if I see a method with the signature

<T> List<T> reverse(List<T> list)

it is reasonable to assume that the function won't use any properties of the type T.

The type signature of a templated C++ function does not appear to offer any hints about its implementation. Is there any feature, existing or suggested for the standard, that would allow us to write function signatures affording similar deductions in C++? For example, some way to say "This function works for absolutely any type".

Answer 1

No, there isn't. Templates are very ad-hoc. Essentially, they are just macros whose expansion is driven by type information. Whether a template can be instantiated with a given type is defined almost entirely based on the expansion. In fact, it is allowed to instantiate a template such that only parts of its expansion would type-check, as long as the other bits are not used.

Whether the expansion type-checks depends on many, many idiosyncrasies of C++, its syntax, and semantics. Due to problematic features like overloading, implicit coercions, casts, and template specialisation, there is no hope for a parametricity property that would give you free theorems.

Some comments have mentioned concepts. However, concepts do not change this property -- they allow to contrain instantiation explicitly, but as before, the absence of such a constraint does not imply that it works for everything.

Answer 2

A template is not a normal thing. It cannot be compiled like one, as C++ doesn't have (and probably will never have) any meaningful template concept as an interface and a static contract between the caller and the callee, like a "forward declaration" for a function. Imagine a world where any function is actually a macro (almost like the horrible #define style but not quite as ill behaved) and has to be expanded to be type checked. This is almost what templates are.

This is also what makes templates so powerful! Templates form a Turing complete language because template instanciation can recurse. It's an horrible sub-language so constexpr was invented to have a clean sub-language for recursive compile time expressions without recursive templates.

You can only reason in term of template instanciation. The "signature" tells you nothing. Like clean lisp like macros, templates are never properly separately compiled, not even with "export template" which required a second run of the compiler after linking.

By the way, the idea, insinuated by one C++ standard committee member, that "export template" was sold to C++ experts as a proper separate compilation for templates, as if they were normal non inline functions, is a hoax; no C++ expert ever believed that.