18
$\begingroup$

Here I read that:

Haskell definitely does not have the most advanced type system (not even close if you count research languages) but out of all languages that are actually used in production Haskell is probably at the top.

So I am asking two things:

  1. which research languages have more powerful type systems than Haskell;
  2. what do they improve.

I am just a programmer, so I don't know many mathematical objects used in type theory, please provide gentle explanations if you can.

Improve this question
$\endgroup$
9
  • 3
    $\begingroup$ What's "better"? $\endgroup$
    – David Richerby
    Aug 18, 2015 at 21:51
  • 2
    $\begingroup$ @DavidRicherby I guess that means more powerful type system $\endgroup$
    – Vitaly Olegovitch
    Aug 18, 2015 at 21:57
  • 2
    $\begingroup$ Once you have proven that a type system is Turing-complete, does it really matter? ;-) $\endgroup$
    – DevSolar
    Aug 19, 2015 at 12:30
  • 8
    $\begingroup$ Turing machines are Turing-complete, why don't you use them for your everyday programming tasks? $\endgroup$
    – gallais
    Aug 19, 2015 at 13:30
  • 4
    $\begingroup$ Do note that the original text mentions languages with more advanced type systems and does not make any assertions wether 'more advanced' is better or worse for a type system. $\endgroup$
    – Peteris
    Aug 19, 2015 at 15:26

3 Answers 3

Reset to default
29
$\begingroup$

The question is somewhat problematic, since it relies on a subjective definition of "better."

Dependently-typed languages such as Agda, Idris, and Coq have a stronger type system than Haskell. This means, you can use the types in these languages to prove strictly more properties about your code than in Haskell. That is, there are more incorrect programs that will be caught.

However, this comes at a price: type inference, and testing whether any values of a given type exist, are no longer possible. This means for these languages, you need to explicitly annotate your code with types. Essentially this boils down to writing your own correctness proofs for your code.

So are these languages "better" than Haskell? They can check advanced proofs of correctness for your code, but they can't automatically prove properties about your code the way Haskell can.

Another research language that is "better" than Haskell is LiquidHaskell. This is basically Haskell with refinement types bolted on top, parsed from special comments.

Refinement types allow you you refine types with properties. For example, instead of having an Int, you can specify {i : Int | i > 0}, giving the type of all positive integers. Type inference is decidable with refinement types, but you can't prove nearly as many correctness properties with them as you can with dependent types.

There are other refinement type systems out there, but I'm not terribly familiar with any of them.

Improve this answer
$\endgroup$
8
  • $\begingroup$ Thank you! Is it possible to prove that Haskell type system is the strongest one that still allows type inference? $\endgroup$
    – Vitaly Olegovitch
    Aug 18, 2015 at 23:11
  • 3
    $\begingroup$ Haskell's definitely is NOT the strongest that allows type inference. The refinement types I've mentioned allow for type inference, and many GHC extensions are being added to Haskell which allow for a slightly stronger type system. $\endgroup$
    – jmite
    Aug 18, 2015 at 23:23
  • 4
    $\begingroup$ On top of this, there are many type systems, and many are incomparable: they will be stronger than Haskell in some ways, but weaker than Haskell in others. There's not a linear ordering of type systems from strongest to weakest. $\endgroup$
    – jmite
    Aug 18, 2015 at 23:23
  • 5
    $\begingroup$ Now I want to prove there is no strongest type system that allows type inference. Must resist proving useless facts. $\endgroup$
    – Andrej Bauer
    Aug 19, 2015 at 7:35
  • 1
    $\begingroup$ The fact doesn't seem useless to me. Knowledge that there exists a strongest type system with type inference would be of great interest, especially if it turned out to be feasible to implement. $\endgroup$
    – rationalis
    Jun 27, 2016 at 18:18
10
$\begingroup$

The ML family of languages (StandardML, OCaml) arise from a similar tradition as Haskell and therefore have similar type systems. They are not exactly the same as Haskell, though, and some of their features might suit you better (there is no such thing as an objectively better type system because type systems in programming languages exist to help humans). Here are some features of OCaml that Haskell either does not have (but might have a corresponding similar concept), or Haskell does have but done differently:

  1. Polymorphic variants.
  2. Objects with depth subtyping and classes.
  3. Functors, which are maps between modules (Haskell has modules), and even first-class modules

And please, there is no need to turn this into an ML-Haskell shootout, or else I will start linking to Bob Harper's blog posts ;-)

Improve this answer
$\endgroup$
9
$\begingroup$

The research language Clean has a better type system than Haskell, because it has uniqueness types. The ideas behind uniqueness types are closely related to linear logic, which is closer to the resource limited "real world" than classical logic.

The anti-research language Rust also has a type system with unique features that are closer to the "real world" than classical pure type systems. Most of the ideas which influenced the type system have been published completely independent of Rust long before it even existed. But the way these old ideas are put together is unique, and would also deserve real research publications, even if known loopholes and inconsistencies exist.

Improve this answer
$\endgroup$
5
  • 4
    $\begingroup$ Somehow "published" and "anti-research" do not go together well. $\endgroup$
    – Andrej Bauer
    Aug 19, 2015 at 7:35
  • 1
    $\begingroup$ Uniqueness is certainly an interesting concept, but IMO it's more about semantics, rather than a type system feature as such. And does this really make the type system strictly better? Can Clean do the newer stuff Haskell has added to its type system, higher-rank polymorphism etc. – are some of these even possible when the type system already needs to deal with uniqueness? $\endgroup$
    – leftaroundabout
    Aug 19, 2015 at 12:08
  • 1
    $\begingroup$ @leftaroundabout How familiar are you with uniqueness types or linear logic? If x has a unique type, then f(x,x) is not well typed, for example. It might be possible to extend Haskell to also support uniqueness types. The move semantics in C++ might also be seen as improving the support for uniquencess types on top of an existing type system. $\endgroup$
    – Thomas Klimpel
    Aug 19, 2015 at 12:36
  • $\begingroup$ I am familiar with C++ move semantics, perhaps that's why my impression of uniqueness is as “not much of a type-system thing”. What I'd find interesting is, do full outward-propagating uniqueness types hinder other features of advanced type system? $\endgroup$
    – leftaroundabout
    Aug 19, 2015 at 14:03
  • 1
    $\begingroup$ @leftaroundabout Rvalue references sound like a type-system thing to me. Why should uniqueness types hinder other advanced type features? In the worst case, those advanced features would simply not apply to uniqueness types. Of course, "real world" features like uniqueness types means going for breadth instead of depth, and the time you spend for going broader will no longer be there for going deeper. But I have the impression that uniqueness types offer a nice balance between theory and practice, so I think the time would be well spend. $\endgroup$
    – Thomas Klimpel
    Aug 19, 2015 at 20:17

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.