I'm not sure why you think that the checking will be painful, it almost sounds like you think that it would be done by the programmer. The whole point of type systems is that they can be checked automatically, so the programmer is prevented from doing something stupid.
Dynamic languages already allow all kinds of modifications that might or might not break invariants or introduce subtle incompatibilities; a type system would only make it safer.
It is also not just a matter of "stopping the program and fixing it". Suppose you are writing a game, and during playtesting you encounter a bug, where something is stuck in an endless respawn loop. In a dynamic language, you could look at the misbehaving code, develop a fix, and immediately observe its effects. This allows you to quickly iterate until you have found a solution that works. Compared to a "stop, fix, retry"-cycle, it's simply going to be faster, even assuming you can reproduce the bug reliably (maybe using some kind of input replay).
I have yet to see a type system that can take a putative implementation of a data structure with arbitrarily complicated invariants, and spits out whether the implementation is correct or not. (Note that Coq, Agda, etc. don't quite fit the bill, because they require the programmer to enter the proof himself, even if these tools can partially automate the process.)
> I'm not sure why you think that the checking will be painful, it almost sounds like you think that it would be done by the programmer. The whole point of type systems is that they can be checked automatically, so the programmer is prevented from doing something stupid.
My point is precisely that type systems aren't normally used to enforce data structure invariants directly. Instead, data abstraction (i.e., the inability to inspect the representation of abstract data types from client code) is used to confine the potential to break data structure invariants to a small fragment of a big program (namely, where the abstract data type is implemented). This is in furious contradiction with the idea of inspecting and modifying anything anytime from anywhere.
Those tend to be the mistakes I make when programming interactively in Python. Forgetting to put a single value into a one-element list. Forgetting to check for None. Misspelling a key in a dictionary. Swapping the order of two arguments in a function call.
Yes, in some cases those properties can only be verified by proving some invariant equivalent to the Collatz conjecture. I'd conjecture that most instances could still be solved by an appropriate type system. I'm not too worried if it can't prevent me from invalidating invariants, so long as it can prevent me from making simple mistakes that are obvious in retrospect.
Those tend to be the mistakes that I take for granted any seasoned programmer can detect and fix almost instantaneously and effortlessly. (Of course, not because programmers are superhuman, but rather because Hindley-Milner is the bare minimum a high-level language should have.) It's pathetic that we're still discussing these in 2017.
> Yes, in some cases those properties can only be verified by proving some invariant equivalent to the Collatz conjecture.
I have yet to see a useful program whose correctness is contingent on the Collatz conjecture being true. But I have seen lots of programs that are much easier to verify by hand than using a type system.
> I'm not too worried if it can't prevent me from invalidating invariants, so long as it can prevent me from making simple mistakes that are obvious in retrospect.
I'm not worried either. I'm just saying that “allow anything to be modified anytime, anywhere” is counterproductive. But if you really want to do it, you can do that in ML and Haskell too: just stuff all your top-level definitions into mutable cells.
Evidently most language creators find it difficult to integrate both interactive programming and static typing, which suggests to me that the problem is not easy. Or maybe there just isn't enough overlap between the groups who value one or the other.
> just stuff all your top-level definitions into mutable cells
That seems like it could be part of a potential solution, but it would require rewriting the program so that everything is implicitly wrapped in the IO monad. And it still doesn't handle the case were you want to add to an existing data type.
Interactivity is one thing. Randomly redefining things is a-whole-nother thing. ML and Haskell are interactive. They just don't stuff absolutely everything in mutable cells like most dynamic languages do.
> That seems like it could be part of a potential solution, but it would require rewriting the program so that everything is implicitly wrapped in the IO monad.
You can't have it both ways: either you have effects and accept that you have effects, or don't have effects and accept that you don't have effects. (IOW, lying is bad.)
If I understand correctly, success typing rejects only programs that will lead to a type error at runtime, but allows all programs that it can't prove incorrect. I think that's an interesting idea and definitely better than no type checks at all, but I'd still like to have a type system that can prove some programs to be type safe, if possible.
This is impossible. Data structures have these little things called “invariants” that require proof to be established. In statically typed languages, abstract data types are used to prevent users from breaking these invariants, by making the representation invisible to anyone but the implementor.
If the data structure underlying an abstract data type can be modified anytime, then every time you patch your program, you would have to check two things:
(0) That the new data structure respects every invariant relied upon by other code.
(1) That either the new data structure is compatible with the old one (which is often not the case), or there are no reachable instances of the old data structure in memory.
This is an even bigger pain in the ass than just stopping the program and fixing it.