Give me an example of a correct program you actually want to write, that a decent static type system. I do have examples of correct programs that almost no static type checker will accept, but I don't want to write those programs. For instance:
if true then 1 else "one"
This is an expression of type int, that yields the value 1. But I don't want to write such crap, because of (i) dead code, and (ii) mismatched types between the the branches (one is an int, the other is a string).
I don't deny that. The problem is not with the idea, it's with the (usual) implementation, which is that if you don't appease the type-checker it won't let you run your program. I'm perfectly fine with a type checker that only gives me warnings but still allows me to run the code even if it isn't satisfied.
Try programming in Haskell. Pretty much all other statically typed programming languages (except ML etc.) get their type systems wrong because all types are really (or <x> null). That's useless for doing type checking, which is why there doesn't seem to be much of an advantage to static typing. Type classes and Hindley-Milner inference make things really nice to use. But it's really the lack of null that makes Haskell's type system actually useful for things other than catching trivial type bugs.
As someone who writes java every day for work but deep down loves dynamic languages:
Static typing has value, but it's massively overstated IMO. Type-checking will only catch the most obvious bugs. Type-checking is mostly redundant with the tests I'm writing anyway, its pretty unlikely that a type error would ever make it to prod, so the benefits seem pretty questionable to me personally.
What languages have you worked with before, with static types?
If it's something like Java, C, C++, etc, then I can see your point, but if you pick any of the languages with type inference (like Elm, Haskell, PureScript, OCaml, F#, etc), then you rarely actually have to write types.
Working with the type system is a different way of working. It's more beneficial to see the compiler as a helping friend, instead of an adversary that is just there to complain.
Personally, I honestly hate every time I don't have a time system to rely on. I don't make any false pretenses that I have the whole program in my head 100% of the time. I don't want to have to think about things that a computer can solve for me, hence I like my compiler to do as much work as possible.
As for unit testing, a type system is never supposed to remove the need for unit testing, and if you see anyone promote a language because of this, they are probably (hopefully) over simplifying. What it does do though, is significantly cut down the need for certain types of tests, since you can model so much more logic via types (ADTs, Union types, etc), and get it checked by the compiler.
As an aside: I simply do not believe you've never run into a type error, unless you've only written projects that 100 lines of code, and even then it's quite easy to run into type errors.
One under-appreciated aspect of static types is that they make certain classes of stupidity a little more difficult, for example, overloading the permissible types on an object's member variable such that every bit of code that uses it needs to do an `isinstance()` check to see if it has the type that particular bit of code wants. Doing this would be tedious in a statically typed language where the sane solution is often the easier solution. This doesn't mean it's hard to write bad code in a static language, just that it's harder to do by accident.
In that case, why not let the computer tell you whether or not the types are reasonably self-evident? That's what static typing is.
(Remember, don't mash up "Java and C++" with "static typing". Java and C++ are not worth mentioning when discussing type systems; they have type systems that get in the way and make it harder to code.)
Unless you are using Haskell or Rust then static typing is a terrible way to check if your program is correct.
You need unit tests to confirm the correctness of your program. And unit tests check most of the types for free. So you don't need static typing after all.
IMO adding static types is good step but it sort of misses the point of modern type systems.
The good thing about types is not that you can just annotate (or not with good inference not) and validate that some type is what you expect it to be. It's that with a proper type system you can develop better abstractions.
The test of whether static typing is useful is pretty simple: Do you ever get type errors when you write code with static types?
If you do (and the errors are not spurious), then the static type system is catching real bugs that would have survived for some length of time in a dynamically typed language.
Moreover, designing the actual type system is at least as hard as implementing the type checker. Coming up with a static type system that is flexible/ergonomic, expressive/powerful, sound, easy to use, and also a good match for mutable state and imperative code is really, really difficult, as demonstrated by C, C++, and Java.
A flexible/ergonomic dynamic type system is trivial in comparison. Soundness is handled at runtime when the exact value of each expression is known, and ease of use is almost a given.
If you have a system where the developers often aren’t sure what it does, how to organize the code, aren’t designing for maintainability, etc., static type checking really isn’t going to help you pick up the pieces afterward.
I like static type checking for what it does, but it solves some little problems, not big ones. (And can cause their own little problems.)
Same can be said of static type checking so what is your point? Are you suggesting that those working in static languages don't need to write tests?
Static type checking generally represents an even lower form of error detection than functional and unit testing does. Sure, it can be convenient to have it, but lately I see a lot of static language novices around here talking about their recent and limited experience with type checking as if they are suddenly experts in the tradeoffs between static and dynamic languages.
If you don't test the behavior of your code then it is wrong. Whether the code could in theory be compiled isn't a very good test case.
Static type checking has a measured bug catch rate of <1%. So the quality of any code where the programmer depends on static typing to verify correctness rather than unit tests is very very low.
reply