Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

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

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?

like image 639
Curry Avatar asked Sep 24 '10 14:09

Curry


People also ask

Which programming language has the best type system?

Definitely C++ and Python.

Is Scala a functional language?

Scala is also a functional language in the sense that every function is a value. Scala provides a lightweight syntax for defining anonymous functions, it supports higher-order functions, it allows functions to be nested, and it supports currying.


2 Answers

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
like image 100
Don Stewart Avatar answered Oct 03 '22 19:10

Don Stewart


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.

like image 39
sclv Avatar answered Oct 03 '22 20:10

sclv