Lots of people have listed good things about Haskell. But in answer to your specific question "why does the type system make programs more correct?", I suspect the answer is "parametric polymorphism".
Consider the following Haskell function:
foobar :: x -> y -> y
There is literally only one possible way to implement this function. Just by the type signature, I can tell precisely what this function does, because there is only one possible thing it can do. [OK, not quite, but almost!]
Stop and think about that for a moment. That's actually a really big deal! It means if I write a function with this signature, it's actually impossible for the function to do anything other than what I intended. (The type signature itself can still be wrong, of course. No programming language will ever prevent all bugs.)
Consider this function:
fubar :: Int -> (x -> y) -> y
This function is impossible. You literally cannot implement this function. I can tell that just from the type signature.
As you can see, a Haskell type signature tells you a hell of a lot!
Compare to C#. (Sorry, my Java is a little rusty.)
public static TY foobar<TX, TY>(TX in1, TY in2)
There are a couple of things this method could do:
in2 as the result.
- Loop forever, and never return anything.
- Throw an exception, and never return anything.
Actually, Haskell has these three options too. But C# also gives you the additional options:
- Return null. (Haskell does not have null.)
in2 before returning it. (Haskell does not have in-place modification.)
- Use reflection. (Haskell does not have reflection.)
- Perform multiple I/O actions before returning a result. (Haskell won't let you perform I/O unless you declare that you perform I/O here.)
Reflection is a particularly big hammer; using reflection, I can construct a new
TY object out of thin air, and return that! I can inspect both of the objects, and do different actions depending on what I find. I can make arbitrary modifications to both of the objects passed in.
I/O is a similarly big hammer. The code could be displaying messages to the user, or opening database connections, or reformatting your harddisk, or anything, really.
foobar function, by contrast, can only take some data and return that data, unchanged. It cannot "look at" the data, because its type is unknown at compile-time. It cannot create new data, because... well, how do you construct data of any possible type? You'd need reflection for that. It can't perform any I/O, because the type signature doesn't declare that I/O is being performed. So it can't interact with the filesystem or the network, or even running threads in the same program! (I.e., it is 100% guaranteed thread-safe.)
As you can see, by not letting you do a whole bunch of stuff, Haskell is allowing you to make very strong guarantees about what your code actually does. So tight, in fact, that (for really polymorphic code) there's usually only one possible way that the pieces can fit together.
(To be clear: It's still possible to write Haskell functions where the type signature doesn't tell you much.
Int -> Int could be just about anything. But even then, we know that the same input will always produce the same output with 100% certainty. Java doesn't even guarantee that!)