Hacker News Reader

Comment by duped | Hacker News Reader

> and warn when the compiler finds a problem but allow the program to run anyway

Your compiler giving you a type check error is saying that the program is meaningless. What is the advantage of running a program that is known to be wrong?

The design of the type system will define what is meaningful/meaningless per type check rule (eg a missing branch which can be a warning vs an ambiguous type inference that means the program cannot be compiled). The question is really whether you want to design a type system that can be checked statically, which to me the no-brainer answer is "yes."

I don't want to have to run the program to know if it type checks. I don't want to have to run it to know what types are in the program, or the signature of functions. I want my tool to tell me when my code is provably wrong, and to prevent provably wrong code from being merged into a codebase without executing it.

View on HN

> Your compiler giving you a type check error is saying that the program is meaningless.

The TypeScript compiler will absolutely give you errors for well-formed programs that are guaranteed* do the right thing with respect to what the author intended and that anyone else can see is correct but that the TypeScript compiler itself doesn't reason about correctly. In instances where this happens, it's very useful to be able to ignore them—just like you might ignore the protests of a misinformed team member who insists that such-and-such won't work, even though it provably will. (Although the alternative of just not using the TypeScript compiler can be a worthwhile decision as well.)

* not to be confused with undefined behavior in C where it might just happen to work with one known compiler/platform combo but break horribly for other valid targets

The cost for this is that programs with type errors must still be specified to have a well-defined semantics. That in turn means that you can't hang useful language features off static types.

For example, TypeScript explicitly declares as a design goal that they don't use the type system to generate different code:

https://github.com/Microsoft/TypeScript/wiki/TypeScript-Desi...

Meanwhile in Dart, you can write:

   double d = 1;

In Dart, doubles and integers are different types with different representations. The above line of code works because if we see an integer literal in a context where a floating-point number is expected, we implicitly treat it as a double literal. Note that there's no runtime conversion here. We can do this because Dart does have a sound type system and is happy to use it for language features.

That's also why Dart (and other statically typed languages) support extension methods while TypeScript does not:

https://github.com/microsoft/TypeScript/issues/9#issuecommen...

If the language gives users the ability to type their code, it's really nice to be able to give them as much value in return for their effort. That means building language features on top of them and using types to generate smaller, faster code.

But languages with unsound type systems or that treat programs with type errors as well formed can't really do that.

> Your compiler giving you a type check error is saying that the program is meaningless. What is the advantage of running a program that is known to be wrong?

Well one bit is you might not be looking at the meaningless part.

Sometimes when doing large refactorings or updates never getting to run, try, or look at anything is discouraging. It's a great feeling when it compiles and everything works (or near enough), but spending two days cycling between compiling and fixing compilation errors is not as enjoyable as e.g. seeing the unit test report's green bar tick up.

Maybe compilers should provide more enjoyable feedback, not just better error messages (though I fully support that movement).

I'm not sure I get what you mean by "you might not be looking at the meaningless part"?

What's the difference between seeing a bunch of test failures and fixing them one by one until the test suite is all green, and seeing a bunch of compiler errors and fixing them one by one until the compiler runs clean?

> I'm not sure I get what you mean by "you might not be looking at the meaningless part"?

For example, you might not be pushing buttons that trigger the meaningless part, but the other parts of the system might still be functional.

> What's the difference between seeing a bunch of test failures and fixing them one by one until the test suite is all green, and seeing a bunch of compiler errors and fixing them one by one until the compiler runs clean?

The difference is in one of the cases a highly qualified professional has freedom to decide _when_ to do the fixes.

If there is a pretty graph or not? (Not joking)

Speaking of which, that WOULD be a cool IDE feature. I always liked the feeling of my junit bar going all green after a big change.

Large refactoring and updates are exactly where strong type systems are the most useful. Make change, fail build, fix build, be happy. Unit tests are still there to turn green when you're done.

I can't think of many worse experiences than my past self trying to refactor Python 2 code. Compared to _any_ type system it's just not even close.

Have you considered reading what I actually wrote rather than just hook onto a pair of words and ignore everything else?

I agree. Sometimes I'm prototyping something or feeling my way down one possible implementation -- it's a lot more efficient to go deep in one area of the codebase and come back to fix up everywhere else later once I'm sure this is the right trajectory. In my day job, I use Flow.js which gives me this and I'm a little hesitant to give that up, given there's no many static type checkers that work this way.

I get the sentiment, but ime this speaks more to architecture and code organization than the merits of static typing. It's always possible to skip type checking by designing the software to be modular enough that unreachable code isn't included in the local build.

Like updating data structures should never result in days of work before you can run simple tests. Create a new build artifact that only pulls in the new data structures and the software modules you're working on (and their tests). If you need to pull in the universe to run any unit tests, they aren't unit tests.

Reply on news.ycombinator.com