What makes Haskell's type system more "powerful" than other languages' type systems?

Question

Reading Disadvantages of Scala type system versus Haskell?, I have to ask: what is it, specifically, that makes Haskell's type system more powerful than other languages' type systems (C, C++, Java). Apparently, even Scala can't perform some of the same powers as Haskell's type system. What is it, specifically, that makes Haskell's type system (Hindley–Milner type inference) so powerful? Can you give an example?

Tapley

It would be easier to answer this question if you gave more details about what you do know. For instance, are you aware of what type inference is, and do you only want to know how Hindley-Milner type inference is different, or do you want to know about Haskell's extensions beyond Hindley-Milner? – Damara

see also: #4048012 – Folliculin

Answer 1

What is it, specifically, that makes Haskell's type system

It has been engineered for the past decade to be both flexible -- as a logic for property verification -- and powerful.

Haskell's type system has been developed over the years to encourage a relatively flexible, expressive static checking discipline, with several groups of researchers identifying type system techniques that enable powerful new classes of compile-time verification. Scala's is relatively undeveloped in that area.

That is, Haskell/GHC provides a logic that is both powerful and designed to encourage type level programming. Something fairly unique in the world of functional programming.

Some papers that give a flavor of the direction the engineering effort on Haskell's type system has taken:

• Fun with type functions
• Associated types with class
• Fun with functional dependencies

Olivenite

Answer 2

Hindley-Milner is not a type system, but a type inference algorithm. Haskell's type system, back in the day, used to be able to be fully inferred using HM, but that ship has long sailed for modern Haskell with extensions. (ML remains capable of being fully inferred).

Arguably, the ability to mainly or entirely infer all types yields power in terms of expressiveness.

But that's largely not what I think the question is really about.

The papers that dons linked point to the other aspect -- that the extensions to Haskell's type system make it turing complete (and that modern type families make that turing complete language much more closely resemble value-level programming). Another nice paper on this topic is McBride's Faking It: Simulating Dependent Types in Haskell.

The paper in the other thread on Scala: "Type Classes as Objects and Implicits" goes into why you can in fact do most of this in Scala as well, although with a bit more explicitness. I tend to feel, but this is more a gut sense than from real Scala experience, that its more ad-hoc and explicit approach (what the C++ discussion called "nominal") is ultimately a bit messier.

Keshiakesia

It would be nice to have Haskell on the JVM to replace Scala, but past attempts have shown that this is either not practical or very difficult (I'm thinking of Jaskell in particular). Some things about the JVM annoy me, like the inability to do tail-call optimization (which Clojure hacked around by providing the recur function). Ultimately, I think the best approach would be to get the industry focusing more on developing the Erlang VM. – Calendra

If you search for a Haskell on the JVM, your currently best option is Frege. – Fish

Scala does tail-call optimization. – Hejira

This is neither here nor there, but scala can opportunistically convert a single function calling itself in tail position into a "trampolined" version. This is less efficient than tail call optimization, and if you have two or more mutually recursive functions calling one another in tail position (a not uncommon occurrence) then it is of no help at all, and you need to rewrite the entire system into a single function with some form of "state" flag. – Keshiakesia

Answer 3

Let's go with a very simple example: Haskell's Maybe.

data Maybe a = Nothing | Just a

In C++:

template <T>
struct Maybe {
    bool isJust;
    T value;  // IMPORTANT: must ignore when !isJust
};

Let's consider these two function signatures, in Haskell:

sumJusts :: Num a => [Maybe a] -> a

and C++:

template <T> T sumJusts(vector<maybe<T> >);

Differences:

• In C++ there are more possible mistakes to make. The compiler doesn't check the usage rule of Maybe.
• The C++ type of sumJusts does not specify that it requires + and cast from 0. The error messages that show up when things do not work are cryptic and odd. In Haskell the compiler will just complain that the type is not an instance of Num, very straightforward..

In short, Haskell has:

• ADTs
• Type-classes
• A very friendly syntax and good support for generics (which in C++ people try to avoid because of all their cryptickynessishisms)

Niall

You should implement accessors and they would throw proper exceptions. – Antiserum

@Trismegistos: Exceptions would turn make mistakes into runtime errors, rather than compile time errors in Haskell. – Niall

@Niall You can still write let Just x = Nothing in ... in Haskell. You won't even get a warning (without a compiler flag). The real advantages of Haskell's type system lie elsewhere. – Cooperative

@YellPika: In your example you would get a run-time error in Haskell rather than strange undefined behavior masking the bug which you get in C++.. – Niall

@yairchu: I was referring to the hypothetical guard-your-fields-with-accessors version. In both cases, the type system doesn't statically prevent errors (where "strange undefined behaviour" counts as an error). – Cooperative

@YellPika: Good point. So with C++ best practices you can get on par to what you get in Haskell for free. But note that if you employ best practices in Haskell you (using pattern matching and higher order functions like fmap) you'll avoid the possibility of this run-time error. – Niall

Actually, implementation of Maybe in C++ is a lot more complicated than this. Here's the real thing: boost.org/doc/libs/1_58_0/boost/optional/optional.hpp. Shear amount of code suggests that C++ type system has some serious weaknesses. – Distal

If you really want to, you can statically check all those things in C++. It's just harder and more verbose. – Myriapod

Answer 4

Haskell language allows you to write safer code without giving up with functionalities. Most languages nowadays trade features for safety: the Haskell language is there to show that's possible to have both.

We can live without null pointers, explicit castings, loose typing and still have a perfectly expressive language, able to produce efficient final code.

More, the Haskell type system, along with its lazy-by-default and purity approach to coding gives you a boost in complicate but important matters like parallelism and concurrency.

Just my two cents.

Tautologize

Answer 5

One thing I really like and miss in other languages is the support of typclasses, which are an elegant solution for many problems (including for instance polyvariadic functions).

Using typeclasses, it's extremely easy to define very abstract functions, which are still completely type-safe - like for instance this Fibonacci-function:

fibs :: Num a => [a]
fibs@(_:xs) = 0:1:zipWith (+) fibs xs

For instance:

map (`div` 2) fibs        -- integral context
(fibs !! 10) + 1.234      -- rational context
map (:+ 1.0) fibs         -- Complex  context

You may even define your own numeric type for this.

Husch

Fibonacci isn't a great example for this since it's only defined for integers afaik – Radionuclide

Yeah, I think Functor would be a great example. – Hackler

Was just a silly example for how easy and natural type-overloading is in haskell. – Husch

This also illustrates "overloading" based on "return type". – Soso

Answer 6

What is expressiveness? To my understanding it is what constraint the type system allow us to put on our code, or in other words what properties of code which we can prove. The more expressive a type system is, the more information we can embed at the type level (which can be used at compile time by the type-checker to check our code).
Here are some properties of Haskell's type system that other languages don't have.

1. Purity.
   Purity allows Haskell to distinguish pure code and IO capable code
2. Paramtricity.
   Haskell enforces parametricity for parametrically polymorphic functions so they must obey some laws. (Some languages does let you to express polymorphic function types but they don't enforce parametricity, for example Scala lets you to pattern match on a specific type even if the argument is polymorphic)
3. ADT
4. Extensions
   Haskell's base type system is a weaker version of λ2 which itself isn't really impressive. But with these extensions it become really powerful (even able to express dependent types with singleton):
   1. existential types
   2. rank-n types (full λ2)
   3. type families
   4. data kinds (allows "typed" programming at type level)
   5. GADT ...

Truett