You seem to confuse type checking with shape-driven optimization. Of course the latter can borrow a lot of terminology from the former and in a typed language you would be stupid not to use your types, but they are different topics. Any decent JavaScript or lisp compiler or interpreter will do the same.
Also what Julia does is not exactly type inference. It is rather a form of specialization. Type inference just gives you the type for an expression using just the syntactical representation. Nothing more.
As an example, if I was to invoke your function f with a floating point number, would Julia not happily specialize it for that too (assuming factorial was defined for floating points or taken out of the equation)? The thing here is, that a type checker needs to know about all the specializations a-priori.
Not sure what you mean by that example. If "f" accepts a float and you give a float it will work. If "f" accepts a number (or t subclass number) it will work since float subclass number. If "f" only accepts int then it will fail since you can't convert a float to int (as in there are no defined promotion/conversion rule from float to int). The type check works just like any language.
Specialization will only occur if there are more than one "f" that handles your type (for example both "f" with a number and with float), and then the compiler will choose the most specialized (float). If you write your Julia program like you would with a static language (for example using over-restrictive types like just float and int) it will return the same error as the static language as soon as it can infer the types (when it leaves the global namespace and enters any function). Using over-restrictive types (and declaring return types for methods) is considered bad practice in Julia, but that's a cultural thing, not a limitation of the type checking.
It happens at compile time in Julia (required for the multiple dispatch to work), the compile time is just interlocked between runtime steps. Calling something with incorrect arguments will fail even if the function is never called during runtime (unless the compiler figures that out using only compile time information and decides not to compile it).
But I understand your point, it's not really like a static language checking as it can't do without running the program, so it's better than fully interpreted (a unit test would catch errors even in paths it didn't take) but worse than static checking (as it can't compile 100% of the valid program at once).
> As an example, if I was to invoke your function f with a floating point number, would Julia not happily specialize it for that too (assuming factorial was defined for floating points or taken out of the equation)?
Yes, but I could then define
bar(x::Int64) = x^2 - 1
and this would create a method which only operates on 64 bit integers.
Now I want to be clear that I'm not saying Julia is a static language, I'm just saying that once specialization occurs, things are much more like a static language than one might expect, and indeed it's quite possible add mechanisms for instance to make a function error if it can't statically infer it's return type at compile time.
Also what Julia does is not exactly type inference. It is rather a form of specialization. Type inference just gives you the type for an expression using just the syntactical representation. Nothing more.
As an example, if I was to invoke your function f with a floating point number, would Julia not happily specialize it for that too (assuming factorial was defined for floating points or taken out of the equation)? The thing here is, that a type checker needs to know about all the specializations a-priori.