3 ms·

> 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 mean

by duped 4y ago

> 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.

masklinn 4y ago
> 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).
- _se 4y ago
  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.
  - masklinn 4y ago
    Have you considered reading what I actually wrote rather than just hook onto a pair of words and ignore everything else?
- Karellen 4y ago
  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?
  - lazide 4y ago
    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.
  - nlitened 4y ago
    > 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.
- duped 4y ago
  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.
- 74ls00 4y ago
  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.
cxr 4y ago
> 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
- munificent 4y ago
  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-Design-Goals 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#issuecomment-74302592 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.

by duped 4y ago

masklinn 4y ago

> 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).

_se 4y ago
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.
- masklinn 4y ago
  Have you considered reading what I actually wrote rather than just hook onto a pair of words and ignore everything else?
Karellen 4y ago
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?
- lazide 4y ago
  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.
- nlitened 4y ago
  > 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.
duped 4y ago
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.
74ls00 4y ago
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.

cxr 4y ago

> 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

munificent 4y ago
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-Design-Goals 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#issuecomment-74302592 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.