Type system power

With more powerful type systems, we can specify constraints at finer levels of granularity. Here are some examples, but don't get bogged down if the syntax doesn't make sense.

In Go, we can say "the add function takes two integers and returns an integer":

func add(x int, y int) int {
    return x + y
}

In Haskell, we can say "the add function takes any type of numbers, and returns a number of that same type":

add :: Num a => a -> a -> a
add x y = x + y

In Idris, we can say "the add function takes two non-negative integers, and it returns a non-negative integer, and its first argument must always be smaller than its second argument":

add : (x : Nat) -> (y : Nat) -> {auto smaller : LT x y} -> Nat
add x y = x + y

If we try to call this function as add 2 1, where the first argument is larger than the second, then the compiler will reject the program at compile time. It's impossible to write a program where the first argument to add is larger than the second. Very few languages have this capability. In most languages, this kind of check is done at runtime: we write something like if x >= y: raise SomeError().

Haskell has no equivalent of the Idris type above, and Go has no equivalent of either the Idris type or the Haskell type. As a result, Idris can prevent many bugs that Haskell can't, and Haskell can prevent many bugs that Go can't. In both cases, we need additional type system features, which make the language more complex.

This is one section of The Programmer's Compendium's article on Types, which contains more details and context.