14
$\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.

$\endgroup$
  • 3
    $\begingroup$ What's "better"? $\endgroup$ – David Richerby Aug 18 '15 at 21:51
  • 2
    $\begingroup$ @DavidRicherby I guess that means more powerful type system $\endgroup$ – Виталий Олегович Aug 18 '15 at 21:57
  • 2
    $\begingroup$ Once you have proven that a type system is Turing-complete, does it really matter? ;-) $\endgroup$ – DevSolar Aug 19 '15 at 12:30
  • 7
    $\begingroup$ Turing machines are Turing-complete, why don't you use them for your everyday programming tasks? $\endgroup$ – gallais Aug 19 '15 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 '15 at 15:26
24
$\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.

$\endgroup$
  • $\begingroup$ Thank you! Is it possible to prove that Haskell type system is the strongest one that still allows type inference? $\endgroup$ – Виталий Олегович Aug 18 '15 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 '15 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 '15 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 '15 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 '16 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 ;-)

$\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.

$\endgroup$
  • 3
    $\begingroup$ Somehow "published" and "anti-research" do not go together well. $\endgroup$ – Andrej Bauer Aug 19 '15 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 '15 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 '15 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 '15 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 '15 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.