Search code examples
c++templatesabstractiontype-systemstype-theory

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


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".


Solution

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