Type Safety is Unit Test Coverage.
Typing is a statically checked test of correctness of your program.
Languages like C give static typing a bad name. Types are not things like 'float', 'int', 'double'. Types are 'degrees', or 'radians'. Types are 'buy', or 'sell', 'price' or 'yield'. Types guarantee that your code executes as you expect, and prevent you from writing incorrect code in the first place.
Is it 100% effective? No. But there's a reason that high level statically typed languages (Scala, Haskell, OCaml) usually work correctly after they compile.
If you write a Rational class and implement it's + method as
def +(other: Rational):Rational = new Rational(0)
Static typing gives you a knowledge about what kind of object you're dealing with without the need to run the code. It's almost completely useless if the "kinds" supported in type system are as broad as 'int', but it does help quite a lot if the type system let's you differentiate between cm and inches.
It still won't help you at all if you have a logic error - and this is where unit tests are valuable.
Personally I find a mixture of Typed Racket and Racket with contracts and unit tests to be the right thing when it comes to producing as error-free programs as possible. I was also pleasantly surprised with Smalltalk, which has no static typing, but because it runs all the time and every piece of code becomes "live" the moment it's written you can use introspection in place of static typing with very similar benefits.
Anyway, static typing is a valuable tool and one way of making software less wrong but it's important to know there are other tools and to use them all when it makes sense.
Sure. Static typing also doesn't help with misunderstanding requirements, or a faulty test in a recursive function. But strong typing, especially in languages where there is no such thing as a NullPointerException, does eliminate entire class of problems. On the other hand, with dynamic languages, you are often a typo away from a runtime error.
I still don't buy in to this trope.
Q: What is true of every single bug in production?
A: It passed both your type checker and your tests.
My bugs got past my type-checker, but only 100 of them. You have 1000 because the 900 my type checker caught, your dynamic language didn't. Then you go and write unit tests for them, and spend a day writing code that my compiler generated automatically for me.
My reasoning in no way implies that. I simply said that I'm sick of this argument that "if it compiles, it works!" Nobody who knows what they are talking about actually believes that, especially not people who design and build statically typed languages!
Each of those would likely have been a runtime error in a language like Python.
Just earlier today, I had to write a short Python script (I normally write Go), and I was bitten by this. I'm used to the compiler telling me up-front when I try to concatenate a string and an integer, or when I misspell a variable name.
Yes, there are other ways around this (and proofreading your code before you write it is a good practice, in addition to tests). But static typing can make development much faster[1].
Even if you claim that you would have caught all of those bugs in unit/integration/system tests (which I simply don't believe - no real-world project has test coverage that's that good), it's much better to catch bugs at compile-time, because (unless you're writing C++) your tests take much longer to run than your code does to compile.
[0] I qualify this to rule out C, which has weak typing as well as memory management issues to complicate things, and Java, which just has a terrible type system period.
[1] In some sense this is all a moot point, because any difference in development speed and/or code correctness between statically-typed and dynamically-typed languages is dwarfed by one's familiarity with the languages in question. The only real way to test this directly would be to use a statically-typed language that allows disabling of all compile-time type checks as a compiler flag or pragma, but few languages do this in a way that'd be straightforward to do a meaningful blind test.
Each of those would likely have been a compile time error in a language like Haskell.
Just earlier today, I was writing some C++ (I normally write Clojure) and I was bitten by this. I'm used to evaluating code in the REPL as I work, telling me up front when I try to concatenate a string and an integer, or when I misspell a variable name.
Yes, there are other ways around this (and proofreading your code before you write it is a good practice, in addition to tests). But dynamic typing can make development much faster[1].
Even if you claim that you would have caught all of those bugs in a type system (which I simply don't believe - no real-world project has types that are that precise), it's much better to catch bugs at run-time, because (unless you're writing Go) your compiler takes much longer to run than your REPL does to eval.
[0]: I qualify this to rule out Python, which has weak typing as well as mutability issues to complicate things, and JavaScript, which just has a terrible REPL period.
[1]: In some sense this is all a moot point, because any difference in development speed between statically-typed and dynamically-typed languages is dwarfed by one's familiarity with the languages in question. The only real way to test this would be to use a dynamically-typed language that has an optional type system as an external tool, luckily quite a few languages do this in a way that'd be straightforward to do a blind test (Typed Racket, Typed Clojure, Erlang w/ Dialyzer).
Why do you consider this a hindrance? Haskell has a lot of issues, but that's really not one of them. You can write a Haskell program and be relatively confident that it's going to work right in a way you simply won't be with, eg, Java. And you don't have to wait until compiling. With ghc-mod and vim/emacs configured, you'll be notified upon saving if you blew up something in the current file. You don't need to run your code in a REPL to find out about it, although GHCi is pretty good. You spend a lot less time figuring out what goes wrong at runtime, although I'll grand you that the tooling is poor enough that you have a bad time doing when it happens.
> I qualify this to rule out Python, which has weak typing
Excuse me? You rule out Python due to weak typing and mutability but disqualify Javascript due to its REPL? This must be sarcasm. I have no comment about Javascript's REPL (which one? node's?), but Python is most certainly not weakly typed, not in the way "weak typing" is commonly understood. As for mutability, they are comparable (except that Python has at least the good grace to throw an exception at runtime if you attempt to access an attribute which does not exist).
Never mind that not even Python or Ruby, and especially not JavaScript, provide sensible useful REPLs with sane code reloading semantics.
People who shit on crappy type systems turn around and then shit on crappy REPLs in broken dynamic languages. I'd take a statically typed language over a language with a bad REPL any day.
And so does Scala...
The try/fail/modify/repeat cycle of REPL-driven-development is what appeals to me. I "get" the value of strongly typed languages, but I'd prefer to opt-in to strictness, rather than have it forced upon me.
Other than for quick scripts I have no interest in dynamic languages now, fully converted to the Typed side ;-)
Ruby and Scala are quite similar in some ways: terse syntax, functional, MOP capable (implicits), mixins (traits), etc., but yes, you have to prove to the type checker that your intentions are correct/sound.
BTW, Go is not that strongly typed. It seems Google engineers don't like strongly typed languages.
I dunno, I have 11 years of python experience, and almost a year of haskell experience. I am more productive in python when doing small (<100 lines) scripting type tasks. But I am noticeably more productive in haskell when writing bigger things. Haskell has a relatively crappy web ecosystem, yet I'm still more productive with snap+postgresql-simple+digestive-functors then I have ever been with any python framework (from zope way back in the day to django and flask). Tasks that are more skewed to haskell's strengths like highly concurrent network servers make the difference even more pronounced.
One can write Scala the same way in a Scala shell.
Another advantage for some strongly typed languages are the complex, yet safe refactorings they enable automatically by a good IDE. This is not universal though, and is a serious downside to picking Scala over Java.
Just one example, code coverage must be 100% for a dynamic language in order to avoid runtime catastrophic failures due to simple typos - like letter transposition. Sure, 100% test coverage is a nice goal, but it's rarely met. In a typed language, you can be 100% sure this won't happen with zero tests.
It's also what makes refactoring so much easier. If I need to rename a method obj.f() to obj.g(), then I can do so safely knowing that no lingering references to f() remain in my code base (else they would fail to type as f() is no longer a valid method).
As you say, 100% code coverage is unrealistic. Having maintained large applications in both static and dynamically typed languages, I feel that statically typed programs are far easier to manage for this reason - that if my code compiles then it means there exist no errors of a certain trivial class, such as typos and references to classes or methods that have been removed.
There are still other errors to worry about, but mitigating those errors can be done effectively without needing to approach 100% code coverage.
val fooList = List(1,2,3)
fooList.map(...)
If you fooList(3), then of course you're hosed, but that's not the type checker's fault ;-)
Whether it is worth the trouble to do this in the type system probably depends on how good your language's type system is and how expensive array indexing bugs are to catch/fix.
In Pascal, the size of an array was part of the type of the array. IIRC, You simply could not write an array index out of bounds bug. This made it a somewhat reasonable choice for a medical device, where an array index out of bounds could be catastrophic. However...
You also could not create a variable-sized array. There was no way even to talk about the type of such an object. (Yes, I ran into that professionally once.) I think this is why Turbo Pascal (and maybe others?) softened that.
In ruby, you have to have close to 100% test coverage because if you don't you can't have any confidence when you refactor. For example, in ruby project, even a simple delegation call needs to be tested, otherwise you may break it without knowing it when you rename the method delegated to.
You don't need to write such test in a Scala project because there is no business logic in a simple delegation and the compiler will check the rename for you, actually the IDE will do the rename refactor perfectly for you.
In general, some of the unit tests devs wrote in Ruby projects are not to test against business logic but to test type matching. For type related refactoring, they actually have to refactor both the code and unit tests. The dilemma here is that if you are changing your unit tests, how confident you are that they are still covering your refactor?
Eh ... what?! Is that some kind of joke?
https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
Sure, assuming you never have to evaluate, convert, merge or do anything with that data. Then you might have some issues when you have expectations on the behaviours of those actions.
Most errors are fairly random. There isn't a pattern to them. Misspellings, misconceptions. Whether your type system catches them depends on the strength of your type system in addition to how you represent things. (Hashmaps vs. records, whether the get call on a Hashmap returns a nil value or an error when the key's not found.)
A strong type system makes it likelier that errors are caught earlier. This may or may not be justified, depending on the application. For some problems, the reduced error-to-failure distance is considerable and it's a huge win.
How did you use scala? Did you write java code in scala as most people with a C++/C#/java background do? Because that would completely explain the rest of your post. In particular, this statement:
>In my experience issues of type safety are rare
I've been doing pretty exploratory, "refactor the hell out of it every other day" kind of coding lately. I would literally rather not program than have had to do it in a language other than haskell. If I were to record this process, I am sure I would come up with several hundred type errors being caught over the course of a week.
>The same types of bugs are going to crop up in Scala, Python, Java, or even Fortran unless you have tests to help you discover those issues.
The obvious example of that being a bad assumption is that static type systems can completely eliminate unexpected NULL errors. It can eliminate "oops I used the count as the X co-ord by mistake" style errors. It can eliminate a huge class of errors that java programmers don't recognize are in fact type errors.
>Logic errors are generally independent of type issues
Which is why it is so nice to let the computer deal with type errors and be able to concentrate on logic errors instead of constantly having to worry about type errors manually.
Nope.
My issue here is that types, once defined, rarely change in any significant fashion. Refactoring is (generally) an exercise in mutation of logic, not so much the underlying types. When types do change the code that operates on them drastically changes as well. We're no longer refactoring at that point, we're re-writing and then the issues more or less disappear.
>The obvious example of that being a bad assumption is that static type systems can completely eliminate unexpected NULL errors.
What? In Scala it is perfectly possible to pass an uninitialized reference to a piece of code. The type checker most definitely isn't going to catch that. It can merely verify that the reference itself is of the right type. This is actually a common runtime error in those languages.
>It can eliminate "oops I used the count as the X co-ord by mistake" style errors.
Just as long as the count and the X co-ord are of different types. Which I'd guess isn't always the case.
> It can eliminate a huge class of errors that java programmers don't recognize are in fact type errors.
I will concede that static type systems do catch some errors that aren't caught by dynamic languages. My belief is that the class of errors they catch are among the most trivial, and most easily caught in testing (unit-testing or otherwise). Thus I simply don't see big gains in either runtime correctness or refactorability. Maybe slight ones, but nothing worth the loss of expression provided by more dynamic languages. This is true of even softer type systems such as Hindler-Milner (although type inference continues to improve, there might be some middle ground here to explore in the future).
There is no doubt some philosophy at play here. The discussion here is much broader than refactoring alone. I for one find that giving up some formal proof about the correctness of the program is worth the freedom dynamic languages provide.
I'll leave my favorite quote on the subject:
"Static type checking limits programs to only expressing things that the static type system can prove are OK, as opposed to expressing things that the human programmer believes are OK. That's the source of both the expressiveness loss with statically checked languages, and the class of runtime type errors which are unique to dynamically checked languages." - Anton van Straaten
NULLs are a non-issue; that's what Option and FP constructs (map, flatMap, etc.) are for.
> I will concede that static type systems do catch some errors that aren't caught by dynamic languages.
Dynamic languages catch NO errors at all, period. You yourself must maintain your own adhoc type checker (unit tests, with 100% coverage) in order to prevent the class of errors that statically typed languages catch from manifesting at runtime.
That's a great quote, actually backs Scala given that you give up pretty much nothing in terms of expressiveness (compared to Ruby, Python, Groovy, etc.) while retaining all of the safety ;-)
That is the exact opposite of my current experience. I'm changing types constantly. As I flesh out more code, I realize I needed to pass an (Account, Client) not just a Client. Now the compiler tells me every single line in every single file where I need to fix the code to handle that.
>What? In Scala it is perfectly possible to pass an uninitialized reference to a piece of code
Because scala has to make bad concessions to java compatibility. Scala itself is fine, but java opens the door to problems. I did not say scala accomplished this, I said static type systems can. Use ocaml or haskell.
>Just as long as the count and the X co-ord are of different types. Which I'd guess isn't always the case.
But you control the types, that is the point. So if you choose not to use the type system, then obviously it protects you from very little. That is not a problem with the type system, it is a problem with you. You could write a program using only strings if you really hated yourself, and you would thus get absolutely no benefit from the type system. But nobody would be silly enough to blame the type system.
>My belief is that the class of errors they catch are among the most trivial, and most easily caught in testing (unit-testing or otherwise). Thus I simply don't see big gains in either runtime correctness or refactorability. Maybe slight ones, but nothing worth the loss of expression provided by more dynamic languages.
I do not believe your earlier claim to not have been writing java in scala now. If you think there is a "loss of expression", you do not have experience with a modern statically typed language.
>"Static type checking limits programs to only expressing things that the static type system can prove are OK
And if you have no idea how much you can express with the type system, then you draw bad conclusions from that.
Over the years I've worked pretty deeply with both static (C++/Java/Scala) and dynamic languages (Python/Ruby). I simply don't agree.
The biggest thing that contributes to refactorability has nothing to do with type safety. Instead unit test coverage, by a mile, is the thing that makes code easy to refactor. In my experience issues of type safety are rare. The same types of bugs are going to crop up in Scala, Python, Java, or even Fortran unless you have tests to help you discover those issues.
I've long felt that type safety is largely a solution to a problem that doesn't really exist. Not in a hugely meaningful way at least. Logic errors are generally independent of type issues, and as such it is code quality and unit test coverage, more than any specific language feature, that lead to highly flexible (and therefore refactorable) code.