There's also a balance between learning new languages for fun and for the insights they give, and wanting to ship.
As an example: Prolog was mind-bending for me when I tried it and I had a lot of fun with it, but I can't imagine using it to build a product (I'm sure other people have though).
Perhaps my first comment sounded more critical than intended. I'm really excited to see where this initiative with set-theoretic types goes, and if it leads to a fully statically typed language then that will be a bonus. If that doesn't happen, then I'm still perfectly happy with the language as it is.
Elixir taught me that I don't need static types as much as I thought.
One use is a spellcheck. Though some bits are in Rust cause backtracking would be too slow.
Another is a game I'm making, the server is in Elixir, and I use erlog to basically program the NPCs in prolog. The game generates events and they are processed into facts if they are perceived by the character.
And with that I can have the system generate goals based on stuff like "I havent seen X at the market for 3 days whilst beforehand I saw X every day. Let me go check on X."
I didn't know Erlang started as a Prolog program basically, but it shows cause they fit together like a match made in heaven.
What I mean by that is, I used to write JS. Transitioning to TypeScript didn't alter my mental model of the language.
Likewise for Python with type annotations.
The only time I've had that happen is with Scala 3's dependent types/type lambdas, but thats LITERALLY called "type-level programming", so it makes sense.