C type checking does not "constrain the call and the function". It looks at existing, fixed types (not constraints on types) and fails or succeeds. I may be misunderstanding you, can you explain in more depth what you mean?
> or they fail to make a match and they rewind and try again with other constraints.
I don't think C compilers ever backtrack during type checking. Again, maybe I'm misunderstanding what you mean?
> The only difference is that C is only doing this unification for the types of the parameters, whereas Prolog is doing it for the parameter values.
Other big differences include the fact that the C compiler does this at compile time as a preparation for execution, while in Prolog this is most of execution; the fact that Prolog has logic variables; the fact that Prolog has arbitrary nested structures that can be unified; the fact noted above that Prolog does backtracking; and, in general, the big difference that Prolog is nothing like C at all.
> Any programming language that has static types but also has an “auto” variable type, where the type is deduced from the use-def and def-use chains that statement live in, is doing absolutely everything Prolog does, and just not exposing the power of it to you. (Hindley-Milner is an even more advanced constraint-solver than Prolog is.)
AFAIK plain Hindley-Milner does only unification but not backtracking, so I would call it strictly less powerful than Prolog. If we assume a backtracking version of Hindley-Milner, we might call it equally powerful to Prolog. I don't see at all how you can claim that it's "more advanced" than Prolog, though.
> (Though, to be clear, if you can program in the type system, as you can in C++, then you do get an exposure to that power, and can write many backtracking algorithms with it.)
I don't know enough about the intricacies of C++ template metaprogramming, but I'm not under the impression that it exposes backtracking as a primitive the way that Prolog does. (Modulo the trivial observation that C++ templates are known to be Turing complete, so you should be able to implement your own backtracking in them.)
So I don't think the above is correct. I don't think there's any language that has built-in SLD-resolution theorem proving that isn't a logic programming language.
And Prolog is not really a constraint solver. Constraint Logic Programming languages have been implemented in Prolog but the concept of "constraint" is not built-in to Prolog.
Nah. Both Prolog and C do a very similar step: they walk through call-sites and function signatures in your code and check them for compatibility with each-other in a way that can constrain both the call and the function, or they fail to make a match and they rewind and try again with other constraints. The only difference is that C is only doing this unification for the types of the parameters, whereas Prolog is doing it for the parameter values.
Any programming language that has static types but also has an “auto” variable type, where the type is deduced from the use-def and def-use chains that statement live in, is doing absolutely everything Prolog does, and just not exposing the power of it to you. (Hindley-Milner is an even more advanced constraint-solver than Prolog is.)
(Though, to be clear, if you can program in the type system, as you can in C++, then you do get an exposure to that power, and can write many backtracking algorithms with it.)