Which research languages have a stronger typesystem than Haskell and why?
The question is somewhat problematic, since it relies on a subjective definition of &quot;better.&quot;
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 &quot;better&quot; 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 &quot;better&quot; 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 &gt; 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.