I think we need new, better concepts to judge type systems by. Eg TypeScript has convincingly shown to a large crowd that soundness isn't an important property for many key goals of static typing, such as programmer productivity, refactoring support, preventing stupid mistakes and navigating large codebases. Soundness was Flow's big claim to fame and it just made day to day programming harder with mostly academic/cosmetic benefits. I'm sure that there's more reasons why TS won the popularity contest, but TS's pragmatic forgiveness surely played a part.
And I don't even see how "decideable" is a desireable property at all. So what if the type checker can infloop? It won't in practice.
At the same time, most people will agree that eg Go's type system is very different from Idris's. They have very different pros and cons, both in terms of how hard they are to typecheck and how great they are to use. In fact I can't think two somewhat popular type systems that could be more different from one another, but if you only read this page you might think they're comparable.
We need words for "totally anal" and "basically Ruby but some typos are caught" and everything in-between.
And I don't even see how "decideable" is a desireable property at all. So what if the type checker can infloop? It won't in practice.
At the same time, most people will agree that eg Go's type system is very different from Idris's. They have very different pros and cons, both in terms of how hard they are to typecheck and how great they are to use. In fact I can't think two somewhat popular type systems that could be more different from one another, but if you only read this page you might think they're comparable.
We need words for "totally anal" and "basically Ruby but some typos are caught" and everything in-between.