I think what's often missing from these arguments is that statically checking (or inferring) homogenous lists is probably one of the most superficial uses of the type system in Haskell (and indeed not the interesting feature most power-users of Haskell are interested in as far as I can tell).
What is interesting is using the type system to specify invariants about data structures and functions at the type level before they are implemented. This has two effects:
The developer is encouraged to think of the invariants before trying to prove that their implementation satisfies them. This approach to software development asks the programmer to consider side-effects, error cases, and data transformations before committing to writing an implementation. Writing the implementation proves the invariant if the program type checks.
(Of course Haskell's type system in its lowest-common denominator form is simply typed but with extensions it can be made to be dependently typed).
The second interesting property is that, given a sufficiently expressive type system (which means Haskell with a plethora of extensions... or just Idris/Lean/Agda), it is possible to encode invariants about complex data structures at the type level. I'm not talking about enforcing homogenous lists of record types. I'm talking about ensuring that Red-Black Trees are properly balanced. This gets much more interesting when embedding DSLs into such a programming language that compile down to more "unsafe" languages.
What is interesting is using the type system to specify invariants about data structures and functions at the type level before they are implemented. This has two effects:
The developer is encouraged to think of the invariants before trying to prove that their implementation satisfies them. This approach to software development asks the programmer to consider side-effects, error cases, and data transformations before committing to writing an implementation. Writing the implementation proves the invariant if the program type checks.
(Of course Haskell's type system in its lowest-common denominator form is simply typed but with extensions it can be made to be dependently typed).
The second interesting property is that, given a sufficiently expressive type system (which means Haskell with a plethora of extensions... or just Idris/Lean/Agda), it is possible to encode invariants about complex data structures at the type level. I'm not talking about enforcing homogenous lists of record types. I'm talking about ensuring that Red-Black Trees are properly balanced. This gets much more interesting when embedding DSLs into such a programming language that compile down to more "unsafe" languages.