What exactly makes the Haskell type system so revered (vs say, Java)?

Question

I'm starting to learn Haskell. I'm very new to it, and I am just reading through a couple of the online books to get my head around its basic constructs.

One of the 'memes' that people familiar with it have often talked about, is the whole "if it compiles, it will work*" thing - which I think is related to the strength of the type system.

I'm trying to understand why exactly Haskell is better than other statically typed languages in this regard.

Put another way, I assume in Java, you could do something heinous like bury ArrayList<String>() to contain something that really should be ArrayList<Animal>(). The heinous thing here is is that your string contains elephant, giraffe, etc, and if someone puts in Mercedes - your compiler won't help you.

If I did do ArrayList<Animal>() then, at some later point in time, if I decide my program isn't really about animals, it's about vehicles, then I can change, say, a function that produces ArrayList<Animal> to produce ArrayList<Vehicle> and my IDE should tell me everywhere there is a compilation break.

My assumption is that this is what people mean by a strong type system, but it's not obvious to me why Haskell's is better. Put another way, you can write good or bad Java, I assume you can do the same in Haskell (i.e stuff things into strings/ints that should really be first-class data types).

I suspect I'm missing something important/basic.
I would very happy to be shown the error of my ways!

Answer 1

Here's an unordered list of type system features available in Haskell and either unavailable or less nice in Java (to my knowledge, which is admittedly weak w.r.t. Java)

• Safety. Haskell's types have pretty good "type safety" properties. This is pretty specific, but it essentially means that values at some type cannot wantonly transform into another type. This is sometimes at odds with mutability (see OCaml's value restriction)
• Algebraic Data Types. Types in Haskell have essentially the same structure as high school mathematics. This is outrageously simple and consistent, yet, as it turns out, as powerful as you could possibly want. It's simply a great foundation for a type system.
  • Datatype-generic programming. This is not the same as generic types (see generalization). Instead, due to the simplicity of the type structure as noted before it's relatively easy to write code which operates generically over that structure. Later I talk about how something like Equality might be auto-derived for a user-defined type by a Haskell compiler. Essentially the way that it does this is walk over the common, simple structure underlying any user-defined type and match it up between values—a very natural form of structural equality.
• Mutually recursive types. This is just an essential component of writing non-trivial types.
  • Nested types. This allows you to define recursive types over variables which recurse at different types. For instance, one type of balanced trees is data Bt a = Here a | There (Bt (a, a)). Think carefully about the valid values of Bt a and notice how that type works. It's tricky!
• Generalization. This is almost too silly to not have in a type system (ahem, looking at you, Go). It's important to have notions of type variables and the ability to talk about code which is independent of the choice of that variable. Hindley Milner is a type system which is derived from System F. Haskell's type system is an elaboration of HM typing and System F is essentially the hearth of generalization. What I mean to say is that Haskell has a very good generalization story.
• Abstract types. Haskell's story here is not great but also not non-existent. It's possible to write types which have a public interface but a private implementation. This allows us to both admit changes to the implementation code at a later time and, importantly since it's the basis of all operation in Haskell, write "magic" types which have well-defined interfaces such as IO. Java probably actually has a nicer abstract type story, to be honest, but I don't think until Interfaces became more popular was that genuinely true.
• Parametricity. Haskell values do not have any universal operations. Java violates this with things like reference equality and hashing and even more flagrantly with coercions. What this means is that you get free theorems about types which allow you to know the meaning of an operation or value to a remarkable degree entirely from its type---certain types are such that there can only be a very small number of inhabitants.
• Higher-kinded types show up all the type when encoding trickier things. Functor/Applicative/Monad, Foldable/Traversable, the entire mtl effect typing system, generalized functor fixpoints. The list goes on and on. There are a lot of things which are best expressed at higher kinds and relatively few type systems even allow the user to talk about these things.
• Type classes. If you think of type systems as logics—which is useful—then you often are demanded to prove things. In many cases this is essentially line noise: there may be only one right answer and it's a waste of time and effort for the programmer to state this. Typeclasses are a way for Haskell to generate the proofs for you. In more concrete terms, this lets you solve simple "type equation systems" like "At which type are we intending to (+) things together? Oh, Integer, ok! Let's inline the right code now!". At more complex systems you might be establishing more interesting constraints.
  • Constraint calculus. Constraints in Haskell—which are the mechanism for reaching into the typeclass prolog system—are structurally typed. This gives a very simple form of subtyping relationship which lets you assemble complex constraints from simpler ones. The entire mtl library is based on this idea.
  • Deriving. In order to drive the canonicity of the typeclass system it's necessary to write a lot of often trivial code to describe the constraints user-defined types must instantiate. Do to the very normal structure of Haskell types, it is often possible to ask the compiler to do this boilerplate for you.
  • Type class prolog. The Haskell type class solver—the system which is generating those "proofs" I referred to earlier—is essentially a crippled form of Prolog with nicer semantic properties. This means you can encode really hairy things in type prolog and expect them to be handled all at compile time. A good example might be solving for a proof that two heterogenous lists are equivalent if you forget about the order—they're equivalent heterogenous "sets".
  • Multi-parameter type classes and functional dependencies. These are just massively useful refinements to base typeclass prolog. If you know Prolog, you can imagine how much the expressive power increases when you can write predicates of more than one variable.
• Pretty good inference. Languages based on Hindley Milner type systems have pretty good inference. HM itself has complete inference which means that you never need to write a type variable. Haskell 98, the simplest form of Haskell, already throws that out in some very rare circumstances. Generally, modern Haskell has been an experiment in slowly reducing the space of complete inference while adding more power to HM and seeing when users complain. People very rarely complain—Haskell's inference is pretty good.
• Very, very, very weak subtyping only. I mentioned earlier that the constraint system from typeclass prolog has a notion of structural subtyping. That is the only form of subtyping in Haskell. Subtyping is terrible for reasoning and inference. It makes each of those problems significantly harder (a system of inequalities instead of a system of equalities). It's also really easy to misunderstand (Is subclassing the same as subtyping? Of course not! But people very frequently confuse that and many languages aid in that confusion! How did we end up here? I suppose nobody ever examines the LSP.)
• • Note recently (early 2017) Steven Dolan published his thesis on MLsub, a variant of ML and Hindley-Milner type inference which has a very nice subtyping story (see also). This doesn't obviate what I've written above—most subtyping systems are broken and have bad inference—but does suggest that we just today may have discovered some promising ways to have complete inference and subtyping play together nicely. Now, to be totally clear, Java's notions of subtyping are in no way able to take advantage of Dolan's algorithms and systems. It requires a rethinking of what subtyping means.
• Higher rank types. I talked about generalization earlier, but more than just mere generalization it's useful to be able to talk about types which have generalized variables within them. For instance, a mapping between higher order structures which is oblivious (see parametricity) to what those structures "contain" has a type like (forall a. f a -> g a). In straight HM you can write a function at this type, but with higher-rank types you demand such a function as an argument like so: mapFree :: (forall a . f a -> g a) -> Free f -> Free g. Notice that the a variable is bound only within the argument. This means that the definer of the function mapFree gets to decide what a is instantiated at when they use it, not the user of mapFree.
• Existential types. While higher-rank types allow us to talk about universal quantification, existential types let us talk about existential quantification: the idea that there merely exists some unknown type satisfying some equations. This ends up being useful and to go on for longer about it would take a long while.
• Type families. Sometimes the typeclass mechanisms are inconvenient since we don't always think in Prolog. Type families let us write straight functional relationships between types.
  • Closed type families. Type families are by default open which is annoying because it means that while you can extend them at any time you cannot "invert" them with any hope of success. This is because you cannot prove injectiveness, but with closed type families you can.

• Kind indexed types and type promotion. I'm getting really exotic at this point, but these have practical use from time to time. If you'd like to write a type of handles which are either open or closed then you can do that very nicely. Notice in the following snippet that State is a very simple algebraic type which had its values promoted into the type-level as well. Then, subsequently, we can talk about type constructors like Handle as taking arguments at specific kinds like State. It's confusing to understand all the details, but also so very right.

  data State = Open | Closed
  
  data Handle :: State -> * -> * where
    OpenHandle :: {- something -} -> Handle Open a
    ClosedHandle :: {- something -} -> Handle Closed a
  

• Runtime type representations that work. Java is notorious for having type erasure and having that feature rain on some people's parades. Type erasure is the right way to go, however, as if you have a function getRepr :: a -> TypeRepr then you at the very least violate parametricity. What's worse is that if that's a user-generated function which is used to trigger unsafe coercions at runtime... then you've got a massive safety concern. Haskell's Typeable system allows the creation of a safe coerce :: (Typeable a, Typeable b) => a -> Maybe b. This system relies on Typeable being implemented in the compiler (and not userland) and also could not be given such nice semantics without Haskell's typeclass mechanism and the laws it is guaranteed to follow.

More than just these however the value of Haskell's type system also relates to how the types describe the language. Here are a few features of Haskell which drive value through the type system.

• Purity. Haskell allows no side effects for a very, very, very wide definition of "side effect". This forces you to put more information into types since types govern inputs and outputs and without side effects everything must be accounted for in the inputs and outputs.
  • IO. Subsequently, Haskell needed a way to talk about side effects—since any real program must include some—so a combination of typeclasses, higher kinded types, and abstract types gave rise to the notion of using a particular, super-special type called IO a to represent side-effecting computations which result in values of type a. This is the foundation of a very nice effect system embedded inside of a pure language.
• Lack of null. Everyone knows that null is the billion dollar mistake of modern programming languages. Algebraic types, in particular the ability to just append a "does not exist" state onto types you have by transforming a type A into the type Maybe A, completely mitigate the problem of null.
• Polymorphic recursion. This lets you define recursive functions which generalize type variables despite using them at different types in each recursive call in their own generalization. This is difficult to talk about, but especially useful for talking about nested types. Look back to the Bt a type from before and try to write a function to compute its size: size :: Bt a -> Int. It'll look a bit like size (Here a) = 1 and size (There bt) = 2 * size bt. Operationally that isn't too complex, but notice that the recursive call to size in the last equation occurs at a different type, yet the overall definition has a nice generalized type size :: Bt a -> Int. Note that this is a feature which breaks total inference, but if you provide a type signature then Haskell will allow it.

I could keep going, but this list ought to get you started-and-then-some.

Answer 2

• Full type inference. You can actually use complex types ubiquitously without feeling like, "Holy crap, all I ever do is write type signatures."
• Types are fully algebraic, which makes it very easy to express some complex ideas.
• Haskell has type classes, which are sort of like interfaces, except you don't have to put all the implementations for one type in the same place. You can create implementations of your own type classes for existing third-party types, without needing access to their source.
• Higher-order and recursive functions have a tendency to put more functionality into the purview of the type checker. Take filter, for example. In an imperative language, you might write a for loop to implement the same functionality, but you won't have the same static type guarantees, because a for loop has no concept of a return type.
• Lack of subtypes greatly simplifies parametric polymorphism.
• Higher-kinded types (types of types) are relatively easy to specify and use in Haskell, which lets you create abstractions around types that are completely unfathomable in Java.

Answer 3

a :: Integer
b :: Maybe Integer
c :: IO Integer
d :: Either String Integer

In Haskell: an integer, an integer that might be null, an integer whose value came from the outside world, and an integer that might be a string instead, are all distinct types - and the compiler will enforce this. You cannot compile a Haskell program which fails to respect these distinctions.

(You can, however, omit the type declarations. In most cases, the compiler can determine the most general type for your variables which will result in a successful compilation. Isn't that neat?)

Answer 4

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:

• Return 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.)
• Modify 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.

---

The Haskell 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!)

Answer 5

A related SO question.

I assume you can do the same in haskell (i.e stuff things into strings/ints that should really be first class datatypes)

No, you really can't - at least not in the same way that Java can. In Java, this sort of thing happens:

String x = (String)someNonString;

and Java will happily try and cast your non-String as a String. Haskell does not allow this sort of thing, eliminating a whole class of runtime errors.

null is part of the type system (as Nothing) so needs to be explicitly asked for and handled, eliminating a whole other class of runtime errors.

There's a bunch of other subtle benefits too - especially around reuse and type-classes - that I don't have the expertise to know well enough to communicate.

Mostly though, it is because Haskell's type system allows a lot of expressiveness. You can do a whole lot of stuff with only a few rules. Consider the ever-present Haskell tree:

data Tree a = Leaf a | Branch (Tree a) (Tree a) 

You've defined an entire generic binary tree (and two data constructors) in a fairly readable one line of code. All just using a few rules (having sum types and product types). That is 3-4 code files and classes in Java.

Especially among those prone to revere type systems, this sort of conciseness/elegance is highly valued.

Answer 6

One of the 'memes' that people familiar with it have often talked about, is the whole "if it compiles, it will work*" thing - which I think is related to the strength of the type system.

This is mostly true with small programs. Haskell prevents you from making mistakes that are easy in other languages (e.g. comparing an Int32 and a Word32 and something explodes), but it does not prevent you from all mistakes.

Haskell does actually make refactoring a lot easier. If your program was previously correct and it typechecks, there's a fair chance it will still be correct after minor emendations.

I'm trying to understand why exactly Haskell is better than other statically typed languages in this regard.

Types in Haskell are fairly lightweight, in that it's easy to declare new types. This is in contrast to a language like Rust, where everything is just a bit more cumbersome.

My assumption is that this is what people mean by a strong type system, but it's not obvious to me why Haskell's is better.

Haskell has many features beyond simple sum and product types; it has universally quantified types (e.g. id :: a -> a) as well. You can also create record types containing functions, which is quite different from a language such as Java or Rust.

GHC can also derive some instances based on types alone, and since the advent of generics, you can write functions that are generic among types. This is quite convenient, and it is more fluent than the same in Java.

Another difference is that Haskell tends to have relatively good type errors (as of writing, at least). Haskell's type inference is sophisticated, and it is quite rare that you will need to provide type annotations in order to get something to compile. This is in contrast with Rust, where type inference can sometimes require annotations even when the compiler could in principle deduce the type.

Finally, Haskell has typeclasses, among them the famous monad. Monads happen to be a particularly nice way to handle errors; they basically give you nearly all the convenience of null without the horrid debugging and without giving up any of your type safety. So the ability to write functions on these types actually matters quite a bit when it comes to encouraging us to use them!

Put another way, you can write good or bad Java, I assume you can do the same in Haskell

That is perhaps true, but it is missing a crucial point: the point where you start shooting yourself in the foot in Haskell is further along than the point when you start shooting yourself in the foot in Java.