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

user_2820239 0
Viewed 236

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

type-theory abstraction type-systems templates c++
4 Answers

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.

user_10977800

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.

user_9638640

Maybe you mean C++20 constraints and concepts: https://en.cppreference.com/w/cpp/language/constraints:

Class templates, function templates, and non-template functions (typically members of class templates) may be associated with a constraint, which specifies the requirements on template arguments, which can be used to select the most appropriate function overloads and template specializations.

Named sets of such requirements are called concepts. Each concept is a predicate, evaluated at compile time, and becomes a part of the interface of a template where it is used as a constraint.

Note that this feature is added in C++20 and only partial supported by GCC.

user_117204140

This is what concepts are supposed to do in C++20. Of course, all existing templates are unconstrained (except via enable_if trickery or similar), so explicitly using an Any concept could be useful to document the intent.

That said, C++ doesn’t have parametric polymorphism anyway: there is no single way to manipulate “values” of a completely arbitrary type, since there are no pointers to references.) Even writing T() makes non-trivial assumptions about a type. The (draft) C++20 standard library therefore provides “generic value” concepts like Movable that are practically useful but provide fewer free theorems.

user_85862270
Related