Hacker News Reader

> success typing puts the burden of proof on the compiler which will only reject a program if it can prove that the program is incorrect [1]. But as far as I know, that approach has not been included in any mainstream programming languages.

Dialyzer, the optional static typing system that is of part of the Erlang distribution, is based on success typing. Here is an accessible introduction:

http://learnyousomeerlang.com/dialyzer

> When you're having trouble justifying at compile time that a property holds, it's not always because you don't know why it holds, but frequently a problem with the type system you have to write the justification in.

Do you have any realistic concrete examples of this? I find this happens very rarely myself (maybe once every few thousand lines of code) and just involves adding a small amount of code along the lines of "throw 'Unexpected error' // this should never happen because ...".

> The advantage of dynamically typed languages is that you are not glued to one specific proof language and don't have to provide proofs for trivial properties, or one-off programs you only need to run once.

For me, type errors for where you've mixed up e.g. string, number or object variables or where you've forgotten to check if a variable is null/undefined before you use it are incredibly common compared to the rare times the type system gets in your way. You would have to (and most wouldn't) write many automated tests to catch all those potential errors if you weren't using a type system for similar robustness. Throwing all that away because of the rare case the type system obstructs you doesn't make any sense to me.

I still think if you're regularly writing code that is hard to justify to a mainstream type checker you're more than likely doing something very wrong and writing code that is hard for others to understand. I'd love to see a realistic counterexample.

I did not intend to imply that I'm regularly writing code that's hard to justify to a type checker. In fact, most of the code I write is in statically typed languages (I'm not some kind of dynamic typing zealot), so I tend to avoid situations that could never typecheck before they occur.

However, I like to use Python for small single-purpose utilities, and in those cases I don't even bother with the optional type annotations, let alone checking them with mypy. Since those programs are so simple that a handful of test cases is enough for 100% path coverage, if the program runs correctly on one case, it's almost guaranteed to run correctly for all others. (Similar to Haskell's "if it compiles, it runs".) Statically checking for type correctness would be pointless, because you can just run the program to find out. It then becomes quite natural to e.g. apply type-modifying transformations in-place, which most type checkers wouldn't allow, since they assume a single fixed type rather than a progression of different types during different stages. (You can get around that, of course, but it requires constantly recreating essentially identical objects to give them a new type.)

For an example of a project (not written by me) where the type checker's rejection of a correctly working program precluded the use of a type checker, see http://www.oilshell.org/blog/2016/11/30.html

> However, I like to use Python for small single-purpose utilities, and in those cases I don't even bother with the optional type annotations, let alone checking them with mypy.

I agree for small utilities and code that's acting as glue between layers that it's convenient to have languages that are loose with what they accept because you can usually manually and exhaustively QA them and because you have no other choice when connecting languages without static type systems. Once you have a large and complex app though, strong typing makes you so much more productive that I honestly can't understand how anyone could argue against strong types.

> e.g. success typing puts the burden of proof on the compiler which will only reject a program if it can prove that the program is incorrect

That describes any dynamic language that does type inference. Type is taken into account for diagnosis and better code, but not as an excuse for rejecting the program just because it isn't fully analyzed.