Explain ML type inference to a C++ programmer

Question

How does ML perform the type inference in the following function definition:

let add a b = a + b

Is it like C++ templates where no type-checking is performed until the point of template instantiation after which if the type supports the necessary operations, the function works or else a compilation error is thrown ?

i.e. for example, the following function template

template <typename NumType>
NumType add(NumType a, NumType b) {
  return a + b;
}

will work for

add<int>(23, 11);

but won't work for

add<ostream>(cout, fout);

Is what I am guessing is correct or ML type inference works differently?

PS: Sorry for my poor English; it's not my native language.

Answer 1

I suggest you have a look at this article: What is Hindley-Milner? (and why is it cool)

Here is the simplest example they use to explain type inference (it's not ML, but the idea is the same):

def foo(s: String) = s.length
// note: no explicit types
def bar(x, y) = foo(x) + y

Just looking at the definition of bar, we can easily see that its type must be (String, Int)=>Int. That's type inference in a nutshell. Read the whole article for more information and examples.

I'm not a C++ expert, but I think templates are something else that is closer to genericity/parametricity, which is something different.

Answer 2

I think trying to relate ML type inference to almost anything in C++ is more likely to lead to confusion than understanding. C++ just doesn't have anything that's much like type inference at all.

The only part of C++ that doesn't making typing explicit is templates, but (for the most part) they support generic programming. A C++ function template like you've given might apply equally to an unbounded set of types -- just for example, the code you have uses NumType as the template parameter, but would work with strings. A single program could instantiate your add to add two strings in one place, and two numbers in another place.

ML type inference isn't for generic programming. In C or C++, you explicitly define the type of a parameter, and then the compiler checks that everything you try to do with that parameter is allowed by that type. ML reverses that: it looks at the things you do with the parameter, and figures out what the type has to be for you to be able to do those things. If you've tried to do things that contradict each other, it'll tell you there is no type that can satisfy the constraints.

This would be pretty close to impossible in C or C++, largely because of all the implicit type conversions that are allowed. Just for example, if I have something like a + b in ML, it can immediately conclude that a and b must be ints -- but in C or C++, they could be almost any combination of integer or pointer or floating point types (with the constraint that they can't both be pointers) or used defined types that overload operator+ (e.g., std::string). In ML, finding types can be exponential in the worst case, but is almost always pretty fast. In C++, I'd estimate it being exponential much more often, and in a lot of cases would probably be under-constrained, so a given function could have any of a number of different signatures.

Answer 3

ML uses Hindley-Milner type inference. In this simple case all it has to do is look at the body of the function and see that it uses + with the arguments and returns that. Thus it can infer that the arguments must be the type of arguments that + accepts (i.e. ints) and the function returns the type that + returns (also int). Thus the inferred type of add is int -> int -> int.

Note that in SML (but not CAML) + is also defined for other types than int, but it will still infer int when there are multiple possibilities (i.e. the add function you defined can not be used to add two floats).