Static typing is beneficial because it allows programs to generate more descriptive compile-time errors, because it removes the need for run-time type-checking, and because it requires programmers to have a better-defined idea of the way their code actually behaves.
Since a [statically] typed language knows the types of all of the variables in a program when the program is compiled, it is able to report every possible typing error at compile-time. A dynamically typed language will also report those errors, but during a program's testing phase, since testing cannot usually test all possible execution paths, not all typing errors may be found, resulting in a buggy program being released. People using the program will not be impressed by typing errors encountered during execution; it implies that the programmer lacked the skill to catch her or his own errors.
Run-time type-checking can be expensive computationally since the interpreter must constantly check types before performing operations. A compiled statically typed language must by definition be free of typing errors, thus making runtime type-checking unnecessary and speeding up execution.
In addition to these machine-oriented advantages, there is also an important programmer-oriented advantage: writing code for [a] statically typed language requires a more concrete understanding of the way a program actually behaves, since a lack of such understanding will lead to immediate feedback (compile-time errors). Code written for a dynamically typed language might compile correctly and be free of explicit typing errors, but may generate strange side effects due to unintended interaction between types. The person who wrote the code for the statically typed language must have described explicitly which types could interact with each other, eliminating that kind of error.
[An additional remark made by another student:
In addition to encouraging better program understanding on the part of the writer, code annotated with explicit types can be easier to read and understand. Type decisions are arguably an important part of program design, not just technical decoration.]
Static typing allows compiled languages such as C++ to catch type errors earlier and avoid run-time argument checking. Inference allows Haskell to determine the type of a function's parameter(s) and return value, relieving the programmer of making exact specifications and allowing for simply polymorphic functions to be written. However, static type checking does induce certain limitations on the language. Two reticular cases [of which only one is excerpted here] where static type-checking decreases the overall appeal of Haskell are given below.
Often, a programmer wishes to declare a variable to be of any [i.e. unspecified at declaration] type. In languages such as C++ this can be done by using a void pointer or a union, but at the loss of type check [at] compile time. Scheme has no type-checking, and thus has no problem with variables of "any type" [quotes added]...
[Additional remarks:
Flexibility and expressiveness are not the only advantages of dynamically typed languages. From the programmer's point of view, these languages tend to be simpler---recall how freedom from having to specify types made Scheme code easy to learn, easy to write and very concise. Dynamically typed languages are simpler than statically typed ones in another important sense: Compile-time type-checking is more difficult to implement than run-time type-checking. In other words, it's often easier to write a compiler for a language like Scheme than for Haskell, C, C++, etc.
As for an argument against type inference in isolation, for the same reasons that explicit typing is advocated above, the program writer should not be freed from having to annotate code with types.]