[imanaccount247]

>I want to question the importance of soundness in type systems

Why? The most common and popular opinion is already that it is not important.

>Suppose you could catch 99% of type-based errors instead of 100%, and in addition, use a compiler switch to see all the case statements where a class of a type is missing. The intended benefit of this system is that it accepts all correct programs.

That doesn't make sense. That's like saying suppose we had a system of math that gave the right answer 99% of the time. How would doing the wrong thing 1% of the time give you the benefit of accepting all correct programs?

>The restrictive nature of static type systems today is legendary

Mythological. Legends are supposed to have some historical root.

>If you can't make your idea work with functors or typeclasses, chances are good there's no way to get it to compile and you have to write functions in longhand.

What does that even mean? That's like saying "if you can't make your idea work with classes or inheritance, chances are good that there's no way to get it to compile and you have to write functions in longhand".

[millstone]

Suppose we insisted in math that all proofs be computer-checkable. There would be no erroneous proofs, but there would also be many correct proofs that could not be accepted or even formulated. Mathematics would suffer overall.

Compiler enforced static typing rejects many correct programs, which is a disadvantage.

[thoughtpolice]

> Compiler enforced static typing rejects many correct programs, which is a disadvantage.

Only if you care about these programs. It is entirely possible many of these 'correct programs' are not useful at all, or arguably useful, or are outside the domain criteria, and rejecting them is fine. This is often a leading motivator behind the design of things like domain specific languages, or designs like MISRA C - many things by design cannot be done, but often those aren't the things we care about, use, or wish to discuss anyway.

On the flip side, there are things type systems enable that I do not think can be actually accomplished in an untyped language - but really, this isn't very interesting aside from being a minor technical factoid, IMO. It's very far removed from the more interesting question of whether or not it's useful to consider these things at all. And it's completely legitimate to say "No, these things aren't worth considering".

[dragonwriter]

> Suppose we insisted in math that all proofs be computer-checkable. There would be no erroneous proofs, but there would also be many correct proofs that could not be accepted or even formulated.

Is that true? Is there a difference between the things which can be proven true in the sense used in mathematics and the set of things which are computable? The limits of proof (e.g., Goedel's incompleteness theorems) and computability (e.g., the halting problem) are at least deeply related, and I'm not at all convinced that your premise here is true.

[the_af]

> Compiler enforced static typing rejects many correct programs, which is a disadvantage.

In practice, however, it is only a theoretical disadvantage. The kind of "correct" programs that get rejected are not very useful.

[Dewie]

> Compiler enforced static typing rejects many correct programs,

Do you have any examples of programs that would be actually useful? I don't necessarily doubt that they exist, but it's not an interesting point if the argument is basically "they exist, but I don't know of anyone in particular".

[ufo]

I think millstone is exaggerating a bit as most programs people write normally can be rewritten without too much pain in a static language with a rich type system. That said, there are some examples of times where your program asks for clever type system features (that are not always enabled by default or add to the learning curve) or where different type system features don't play nice together (so its hard to have both features in a single static language, but in a dynamic language you can use one style of programming at a time and never notice the problem).

In the first category, one example is programs requiring higher-rank polymorphism. They are always allowed in untyped languages but in Haskell this feature is hidden behind a language pragma to keep type inference simpler by default.

On the second category, an example I like is parametric polymorphism vs subtyping. The type system gets really tricky if you try to use both at the same time so most static languages either limit the polymorphism or don't allow subtyping. ON the other hand, in a dynamic language you can use both styles if you want, although you have to do so at your own risk.

[imanaccount247]

The problem is that your supposition is just made up. There's nothing to support it. Saying "suppose some thing that isn't true" does not support an argument about reality.