tl;dr summary: they are more powerful, more expressive, and most importantly, they don't lie.
[Aside: I would like to point out that there is a double false dichotomy in the OP's question.
- FP and OO are orthogonal, not alternatives. FP is about not having side-effects, OO is about behavioral abstraction. You can have behavioral abstraction without side-effects, which gives you OO and FP – indeed, William Cook has (only half) jokingly argued that since the only abstraction mechanism in λ-calculus is the function, all abstraction in λ-calculus is automatically behavioral and thus λ-calculus is the first and purest OO language. (And indeed, if you see how e.g. booleans are implemented in Smalltalk, the implementation is basically identical to the Church Encoding of booleans in λ-calculus, or viewed from the other side, in the Church Encoding of booleans in λ-calculus, the values
true and false act at the same time as conditionals … something that is at the same time a value and behavior smells very much like an object!)
- There is nothing that stops a non-functional (IOW imperative) language from having a powerful, expressive, strong, strict, static type system. It's just much harder to design one. Type system designers are just as lazy as every other programmer, so FP languages tend to have the better type systems because it is easier to design a better type system for them.
]
There is an interesting correspondence between computer programs and logic systems. This was first noticed independently by Curry and Howard, and is now known as the Curry-Howard Isomorphism. In a certain mathematical sense, a program written in some programming language is isomorphic to a proof in some formal logic; a type in some programming language is isomorphic to a proposition in some formal logic: a proof is a program, and the formula it proves is the type for the program. The return type of a function corresponds to a theorem, the parameter types correspond to the hypotheses, and the function code corresponds to a proof that given the hypotheses, the theorem holds.
Since every type system gives rise to a system of logic (and every system of logic gives rise to a type system), we can look at different type systems by looking at the systems of logic they induce.
But I won't go deep into mathematical logic and type theory here, not the least because I am neither a logician nor a type theorist. I'll try to stay on the practical side.
Intuitively speaking, you want your type system to induce a system of logic that is consistent, i.e. that doesn't allow false theorems to be proven. The more inconsistent the system of logic induced by the type system is, the less useful the type system is as a proof of correctness of the code.
Now, let's look at a couple of (simplified) languages. Let's start with a language like Idris, for example. In Idris, when a function has a return type of String, it always returns a String. Now, you might say that's obvious, of course a function that is typed as String returns a String … but does it, really? Is it really that obvious?
Let's look at Java! Here's what a method typed as String can return in Java:
- a
String
null- an exception
- and it can even not return at all (e.g. run into an infinite loop)
- in addition to that, it can also return a "modified state of the world" (e.g. it can print a line of text to the console)
So, there are several ways for a method in Java to not return a String (either not return at all, return nothing, return something else, return something in addition, or several combinations of the above) even when its type says so.
I said above that there is a correspondence between programs and logic, and without going into the mathematical details of what all of this means, you can certainly imagine what happens when you try to prove something using a system of logic that allows you to "lie" like that!
A similar thing applies to the parameter types: a method that has a parameter of type String can also take null as an argument, and in addition to that, it can open a database connection, open a file, open a network connection, read from the console, use a random number generator, use reflection, all to get additional inputs, which do not show up in the parameter list.
This gets even more obvious when we throw Parametric Polymorphism (called Generics in Java) into the mix. Parametric Polymorphism means that functions know less about their types than when the types are concrete; ironically, this allows us, as the programmer, to know more about what the function does from just the types. A typical example that is often given to demonstrate the power of parametricity, is this mystery function:
mysteryFunc :: (a, b) → a
or in Java syntax:
<A, B> A mysteryFunc(Pair[A, B] p)
What does this do? What is the name of this function? Now, you might say, how can you know that from just the types, without any documentation, without the name, without the code, but the thing is: you can, thanks to parametricity. The function gets passed a pair of values, one of type a and one of type b. What can the function do? It can't return the second value, it is of the wrong type. It can't get a value of type a from somewhere else, because there is no "somewhere else" – if it wanted to get an a from a database, for example, it would have needed to take a DB handle as an argument. It cannot construct an a, because a is a type variable: the function doesn't know anything about a, and how is it going to construct something it doesn't know what it is?
So, the only possible thing it can do, is return the a it was passed – in other words, this is the fst function, which returns the first element of the pair it was passed.
There are other examples, e.g. a → a can only be the identity function, there is no other function that has this type.
Now, none of this is true in Java. The Java method can go and retrieve an A from a database, it can use reflection, it can do lots of other things.
If we assume not only such a "logical" type system, but also a "logical" programmer, it gets even more interesting. Let's take the following function type:
Bool → Bool
There are several things this function could do:
- return the boolean that was passed in
- ignore the boolean that was passed in and return a constant
- return the result performing some operation on the boolean that was passed in
Now, as you noticed, without parametricity, there is a lot less we can say about the function. However, there are a couple of things we can assume:
- This is just the identity function for booleans. It doesn't make sense that a programmer would write it that way. Either there is an already existing identity function in the standard library, then she would use that; or there isn't, and she really needs to write it herself, but since the function doesn't actually look at the value at all it doesn't care what type the value has, and it would have the more generic type
a → a.
- Similar to above: if the function ignored its argument, there wouldn't be a need for the argument to be a boolean, and the type would be
a → Bool.
- So, this leaves us with option #3: the function returns the result of some operation on the value; the only unary operation on booleans is negation, so this is the
not function.
This is much less strong than our result for the fst function above, since it does not rely solely on the logic of the type system, but also on the "well-behavedness" of the programmer.
There are some important things that make all of this work:
- Parametricity
- Referential Transparency / Purity
- Totality
Java doesn't have full Parametricity, there are things you can do with values even if you don't know their types, for example you can test for reference equality (==), you can convert it to a string, you can compute its hash code, you can cast it. Worst: you can get its class, then get that class's constructor, and construct a new one.
Java also doesn't have Referential Transparency / Purity (which essentially means that the value of an expression or the return value of a function depends only on its constituent sub-expressions or the input arguments to the function; it also means that any function call and any expression can be replaced with its value everywhere in the program (and vice versa) without changing the meaning of the program; intuitively, it means that functions and expressions cannot have side-effects). So, not only can Java construct a new a using reflection, for example, but it can also print to the console, mutate global state and do pretty much everything it pleases.
That's why when presented with a signature such as a → a, all we can say is "this could do literally anything, including launching the proverbial nuclear missiles".
Now, Haskell does have Parametricity and Referential Transparency, so in Haskell, we can say a lot more, specifically, we can say that if this function returns, then it is the identity function. IOW, it can either return its argument, or it cannot return at all (e.g. infinitely recurse). There is no other option. These are the only things it can do.
Idris, additionally, is Total, which simply means that functions are defined over all their argument values, i.e. they always return a value. This removes the last alternative, and means that a → a can only be the identity function. (Incidentally, this also means that Idris is not Turing-complete, but that is actually not a big deal: Idris is "Tetris-complete", meaning it can do I/O, it can do Foreign Function Calls, it can do interactivity.)
[Note: technically speaking, Idris is not Total. You can write non-terminating programs in Idris, however, Idris will tell you if it cannot prove that your program will terminate, and then it will no longer guarantee that any other proof it makes is correct.]
So, this is one piece of the puzzle: the fact that a program type checks tells you a whole lot more about the program than it does in e.g. Java. A function that has type String and type checks really does return a String and doesn't do anything else. This means that you can have a lot more trust in the types, and the types can tell you a whole lot more about the program.
We can say that, since types are theorems and programs are proof, we can have more confidence that the proof is correct.
The other piece of the puzzle is that type systems such as Haskell's or Idris's are much more expressive. So, not only can you have more trust in the proofs and the theorems, but the theorems you can write are also more "interesting"! I mean the fact that a function that claims to return a String really does return a String is a nice property to have in and of itself, but the statement "Hey, I return a string" is something you can also write in Java. (You just can't guarantee it's true.)
[Note that these are two orthogonal aspects: what I talked about above could be called the "strength" or "strictness" or "trustworthiness" or "power" of the type system. It refers to how strong the "claims" are that I can make about the program, how much I can trust these claims. Whereas the next aspect refers to how "sophisticated" the claims can be. We might call this the "expressiveness" of the type system.]
However, the type systems we are talking about here, can express much more interesting properties. At the extreme end of the scale are dependently-typed languages which can express any property that you can express using formal logic as a type, and then consequently type-check it. For example, in a dependently-typed language you can express the fact that a function that zips two lists preserves the lengths of the list, you can express the fact that a function that concatenates two lists returns a list whose length is the sum of the lengths of the input lists, you can express the fact that a function that sorts a list returns a list that is, in fact, sorted, has the same length, and the same elements as the input list.
For example, the Idris standard library has a Vect type that is a list that also carries its length in the type. Here's the type of the append function:
app : Vect n a -> Vect m a -> Vect (n + m) a
As you can see, the collection is not only parameterized over its element type (like e.g. a Vect<A> in Java), but also over its size, which is a runtime value! Imagine a Vect<A, n> in Java that is instantiated like new Vect<String, 3> … pretty crazy, huh? Dependently-typed languages are called "dependently-typed" because static types can depend on runtime values – this is the ultimate in expressive power, and essentially blurs (or rather obliterates) the distinction between Automated Theorem Proving and programming: a type can express anything that logic can express, which means everything you would normally write in a formal specification document, you can instead write as a type. And if the program compiles, then it is at the same time also a correctness-proof of its implementation wrt. the specification.
However, not all languages are dependently-typed. Most other type systems, such as Haskell's or ML's lie somewhere in between. But still, there are some interesting things that can be done with types. For example, there is a company called Galois in the US that does interesting things with Haskell; among other things they have a document management and document sharing platform for government organizations where they have encoded the rules for distributing classified documents into the Haskell type system. You literally cannot write code that accidentally (or even purposefully) leaks classified documents or distributes them to the wrong people: it simply wouldn't compile, it would be a type error.
So, there you have it:
- the types are more reliable in that they actually ensure that what they claim is true
- the types are more expressive in that you can claim more interesting properties
