Lambda the Ultimate

The thing about templates in C++ is that code is generated for each instantiation. That is, even if you don't overload, you still will get a new set of code generated for each type you use the template with.

And this is the only way C++ style overloading can work. What if you write a generic function f that is overloaded for a specific type. And then you write a generic function g that calls f but is not itself overloaded for that specific type.. Well, it cannot generate the same code for g for all types. It must generate code for each type, because it must call the correct version of f. Etc.

C++ templates were my first introduction to parametric polymorphism (or at least the first introduction that I understood) and they blew my mind when I encountered them. But after working with the equivalent in ML and Haskell... C++ templates really seem kind of silly and way too complicated. The whole mechanism of doing parametric polymorphism by textual inclusion of the function/class definition, and creating code for each instantiation, is just bogus. I suspect that the reason that particular mechanism was used is just because in C++ nothing is boxed, and so types have different sizes. In fact I actually think that a lot of C++'s bogosity is due to trying to shove features into the language without boxing things.

I believe that if you want different code depending on what type you are using, what you want is probably either OO or Haskell-style type classes or something along those lines... not parametric polymorphism.

Things become easier when you realize that the term parametric polymorphism means different things in each of these cases. The concepts are related but distinct.

Can muliple implementations of template T f(T x) {...} be created (while being truely parametric)? I can't see it. I'm thinking f still has to be the identity function.

That may be a large chunk of your confusion. C#/Java generics should be (actually they should be bounded parametric polymorphism). C++ templates allow you to cover the cases that parametric polymorphism covers (it "subsumes" parametric polymorphism, at least the first order case), but it is not possible to determine whether a function is truly parametric by looking at its type, i.e. parametricity is effectively lost (of course, it's significantly weakened anyways due to side-effects). Here's some code to compare:

template <typename T>
T id(T x){ return x; }

does have exactly the same parametricity properties as the Haskell function,

id :: a -> a
id x = x

but,

template <typename T>
T f(T x){ return x*x; }

has exactly the same type, but has dramatically different parametricity properties, it's kind of like the Haskell function

f :: (Num a) => a -> a
f x = x*x

As you can see in the Haskell version (or in the C#/Java version using bounded parametric polymorphism), it is clear that we are not talking about any a, but only those that can be multiplied. f's type in Haskell is different than id's type. This is not the case in C++, their types are exactly the same. This means that you can make effectively no assumptions about a function given just it's type (assumptions related to parametricity that is). Furthermore, the function can make arbitrarily complex assumptions about the type of its arguments and not reflect that in the type at all, hence all those boost macros and template chicanery to try to make it clearer what exactly the expected assumptions are. As I said, while side-effects weaken parametricity properties we can still make some assumptions, i.e. a function forall a.a -> String, say, in a language with side-effects still cannot make any use of it's argument, however it is not required to be a constant function as it would be in a pure language.

It would seem like in addition to identity, that "bottom"-returning functions would be acceptable, for whatever the language's various bottoms might be. In Java, for instance, a function that never returned, a function that immediately threw an unchecked exception, and a function that simply returned null could all be validly typed as a->a, all without introspecting or bounding a. Is it provable that no such functions are valid in languages with Hindley-Miller type inferencing?