Sure — for context I’m very comfortable with Haskell, Typescript, Java and Scala, fairly comfortable with Agda, Coq, C and Rust. I don’t prefer
Python (the reasons of which I can elaborate, if you’re interested), but I do prefer to do my programming in Lisp-like dynamic languages —
even when not using meta-programming.
The reason for this is quite simple. A static type-system, by design is meant to invalidate programs which are incorrect and accept the programs
which are correct. All static type-systems which exist invalidate a certain number of programs which are correct — that is to say, you can
write a perfectly valid program, but the type-system can reject it. What we term to be a more expressive type-system, is one which rejects
more programs. The line which one draws in the sand as expressive enough is completely arbitrary and the type-systems we have currently
heavily rely on the user constructing their programs in a certain way, so the type-system can prove certain properties about it.
Here’s an example demonstrating what I mean. Consider a theoretical language which uses : as the type-ascription,
has generics/kinds and all functions are total. A code-snippet taking the head of a list might look like this:
> let num: Option = head(numberList)
Note that the return type of the head will be Option, if the function is total because the list can be empty. Now suppose I have the snippet —
locally I can reason that the type of num should be Number — but I need to prove that to the type-system. In most current type-systems, proving
this requires you restructure your code in a particular way.
> let numberList = prependList(4, previousList)
> let sortedList = sortList(numberList)
> let num = head(sortedList)
What I’m trying to drive at is that static type-systems are a spectrum and at some point you will run into a case which you’ll either
need to use an escape-hatch or restructure your code in a non-trivial way to satisfy the compiler. The boundary of what you determine
to be correct is also completely arbitrary — you can always encode more properties and restrict your code further; how far you
go is ultimately determined by you.