Earlier quoted context omitted.
Sure, you can encode various properties in some languages, but it's not that common to actually do so.
In Haskell, it's both common and idiomatic. There's always a tradeoff between the usefulness of having static guarantees, and the complexity of the type system features that enable those guarantees. In some cases it's more trouble than it's worth to enforce certain static properties - you have to weigh the costs and benefits on a case by case basis. But it's nice to have the option, and Haskellers make use of it freq…
If the code is sound, it should have the same complexity anyways. I.e. putting a non-empty requirement in the function signature is just as complex as adequately handling an empty array in the code.
My personal struggle is that statically typed languages are annoying to prototype (I don't care if it segfaults on my laptop, I want to validate my idea). My struggle is prototyping in something that I can easily transition to a strictly typed version. I'm curious to try prototyping in Javascript and adding types when I move to production.