Which research languages have a stronger typesystem than Haskell and why?

Problem Detail: 

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.

Asked By : Vitalij Zadneprovskij

Answered By : jmite

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.

Best Answer from StackOverflow

Question Source : http://cs.stackexchange.com/questions/45383