[Solved]: How can SML infer types like this?

Problem Detail: 

Wikipedia says:

fun factorial n =      if n = 0 then 1 else n * factorial (n-1)  

A Standard ML compiler is required to infer the static type int -> int of this function without user-supplied type annotations. I.e., it has to deduce that n is only used with integer expressions, and must therefore itself be an integer, and that all value-producing expressions within the function return integers.

I don't understand how a compiler could infer this. It sounds like SML is essentially solving the halting problem for the factorial function, and showing that it only halts on positive integer inputs.

Am I missing something?

Asked By : Xodarap

Answered By : didierc

The classic Hindley-Milner type inference algorithm requires each literal value to be unambiguously inferable to a type: 0 is an int, while 0.0 is a real. Haskell's type system has been enhanced to include a certain kind of bounded polymorphism, so that 0 can have any type that is a number (more precisely, of any type that is an instance of the Num type class: 0 is of type Num a => a).

See the wikipedia article on Hindley-Milner for further details on the algorithm (the article explanations are much better than anything I could write on that topic).

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/9407