There are of course the ordinary people do what they do reasons: familiarity with the language, consistency within a project, opinion and deep insight into the problem and dumb mistakes.
Static typing offers some advantages in regard to tooling. Entire classes of errors can be caught by the editor/IDE as the programmer types code without waiting for compile time...or in the case of dynamic languages perhaps runtime.
ML languages are particularly suited for the classes of problems for which they were developed, e.g. fault tolerant high reliability systems, because they can efficiently express state machines via pattern matching semantics and the SOME|NONE construct.
So a person might choose to write a web application in F# because they are thinking about the problem in terms of a state machine. With code generation, a stack similar to Microsoft's can provide a lot of the Presentation and Storage layers in Javascript and SQL respectively.
> ML languages are particularly suited for the classes of problems for which they were developed, e.g. fault tolerant high reliability systems
Are you thinking of Erlang? Erlang is definitely not a ML, although they share some similarities (immutability, pattern matching). Not sure what ML originally was designed for, other than maybe building compilers.
> So a person might choose to write a web application in F# because they are thinking about the problem in terms of a state machine
Algebraic data types in ML allow you to encode program state within the type system, so the compiler can help ensure the program is in a consistent state at any point during run-time. That is the real benefit to having a strongly static type system in the vein of ML.
Regarding the original question: the difference between static and dynamic types is, IMO, one of checking at compile-time vs run-time. (But the static/dynamic definition is fuzzy enough that there's often leeway for interpretation here.) Type inference is icing on the cake -- type annotations could be explicit (C, Java) or implicit (ML), but a language is not statically typed unless the types are known prior to execution.
> Are you thinking of Erlang? Erlang is definitely not a ML, although they share some similarities (immutability, pattern matching). Not sure what ML originally was designed for, other than maybe building compilers.
ML stands for metalanguage. It was originally developed for a theorem prover. I think the expressibility of the ML family of languages turned out to lend themselves to many categories of programming problems like compilers. Especially since the code could so closely match the structure of the problem itself (via recursion, pattern matching and other features).
EDIT: Commenting on my point about code matching the problem structure. This is why I'm, in general, a fan of most functional and declarative programming languages I've tried. Prolog, Common Lisp, Scheme, SML, Ocaml, Haskell, Erlang, etc. They may not be ideal for every problem (though the malleability of Scheme and CL make them pretty damn close, IMHO), but there are a number of domains where they truly excel compared to the bog-standard enterprise languages. The only problem I have not solved is convincing bosses to accept a polyglot environment. They seem happy with Python and C++ and C# and Java, but throw in even F# and they reject it.
Erlang came from Ericsson, SML from Bell Labs. Erlang's contract based programming idiom is another, and perhaps better, approach to high reliability fault tolerant system implementation, but though I was thinking about it by virtue of thinking about software for high reliability fault tolerant systems developed by telecoms, rest assured I was not writing about it. The reason I wasn't writing about it is that it would not have answered my comment's parent.
Sure, the only reason for mentioning Erlang is because "high reliability and fault tolerant systems" are its raison d'etre, but AFAIK that's not an expressly stated design goal for any of the ML languages. Any such benefits come as a side effect of ML's design. However, a lot of ideas from ML are being incorporated into (non-ML) languages that do have reliability and safety as a design goal, such as Rust.
With :pre and :post, Erlang's design by contract has made it's way into Clojure...and in the form of a full featured contract system, into Racket as well.
Static typing offers some advantages in regard to tooling. Entire classes of errors can be caught by the editor/IDE as the programmer types code without waiting for compile time...or in the case of dynamic languages perhaps runtime.
ML languages are particularly suited for the classes of problems for which they were developed, e.g. fault tolerant high reliability systems, because they can efficiently express state machines via pattern matching semantics and the SOME|NONE construct.
So a person might choose to write a web application in F# because they are thinking about the problem in terms of a state machine. With code generation, a stack similar to Microsoft's can provide a lot of the Presentation and Storage layers in Javascript and SQL respectively.