Strong Static Typing with Type Inference

Virtually every modern language, excluding C and C++, gives you strong typing. Strong typing means you can't accidentally treat one type as another and have it go unnoticed until you get garbage in your data or a core dump. But many languages, and most "scripting languages" give you strong dynamic typing, which means that you pay for strong typing at runtime in wasted memory (your data are all tagged with type information) and wasted cycles (your data are repeatedly type-checked upon every operation). Worse, none of this prevents type errors from occurring at runtime (perhaps months after testing and productionization) -- it just means that the runtime error will clearly explain that it is in the nature of a type conflict: small consolation when your application is broken.

Static type checking means that the compiler knows your data types at compile time and won't allow you to compile a program with type conflicts. This allows the compiler to save memory by eliding type fields on data, and to not bother checking types with each operation, thus saving time. This can all be done safely without fear of core dumps. More importantly, once your program compiles, an entire, very large, category of bugs is eliminated: of course your program may still contain bugs that will cause it to blow up at runtime -- failed assertions, infinite loops or recursions, logic errors, domain errors, out of memory, deadlocks -- but it won't be blowing up because you passed an integer to a function that expects a string.

Many modern languages feature static type checking -- Java is one -- but nearly all of them require you to pay for this benefit by writing explicit type declarations for each variable and for the domain and range of each function you define. And you must keep these declarations up to date and in sync as you develop and modify your program. Of course, in most any language, when you change the domain of some function you need to chase down and change every call to that function, but in addition to that work, you need to also make sure to (correctly) modify all the affected type declarations too. Many programmers consider this to be mere "bookkeeping" of the most tedious sort, which I guess explains why many modern languages (and most scripting languages) are dynamically typed and don't have type declarations.

OCaml gives you the best of both worlds. It's statically typed, with all the benefits that entails (including a good part of the speed of OCaml's compiled code), but you don't need to write explicit type declarations (unless you want to), because the compiler infers your types for you. If you use your functions and data inconsistently, OCaml detects this and gives you a type error, at compile time, so that you can correct the problem. All with no bookkeeping.

I can't speak highly enough of this feature. I find that my debugging time is significantly lower because OCaml eliminates this class of runtime errors, and forces me to actually understand the code I write (where dynamically typed languages encourage me to just dive in and start testing, hoping for the best). Finally, I'm amazed at the way my code tends to be correct once I get it to type check successfully -- this happens at both the micro-level (i.e., at the level of individual functions) and (less so, but still significantly) at the macro-level (i.e., whole modules and applications).