The expressions x - y and y - x often have exactly the same type tree, but calculate a different value. Same with f(x, y) and f(y, x) when the parameter types are the same.
To actually catch real bugs such as this with types, you have to make such a fine grained use of types that programming becomes nigh intractable.
If x has type minuend<integer> and y has type subtrahend<integer> then, x - y is well typed, whereas y - x isn't. Problem is, the values come from some other context in which their minuend and subtrahend are meaningless (and, in any case, are not involved).
The kinds of errors that are found by static typing in practice are those that, under dynamic typing, will only sneak into production if the code is not tested at all. I.e. if the code had been executed even once with any inputs, the problem would have showed up.
Plus, if you assume that "dynamically typed" language means "language with no static checks", you're arguing against a strawman of dynamic typing. That is even more ridiculous if you're pitting True Scotsman's state-of-the-art static typing against this dynamic strawman.
(Of course, some dynamic languages in widespread use do more or less look like that strawman; however, the best examples of dynamic typing are languages which are considerably informed about type prior to executing a program, like the SBCL dialect of Common Lisp, for instance.)
Typing has its place but the idea that it catches all bugs at compile time certainly isn't true; the cycle of running the app itself, running its tests, is just as important for statically-typed code as dynamically typed.
Languages that have a sophisticated contract system* (like Clojure's Clojure.spec library) have a bit of a leg up in my opinion. You can much more precisely explain and control and test for the specifics of all values flowing through your system well beyond merely what type they are.
-- * Clojure's devs don't refer to spec as a contract system because it is quite a bit more versatile than that, and some are actually using it for compile-time checks, compile-time generative testing, and other nifty things that aren't covered by a "contract" system.
Of course it can. The idea behind a decent type system is to make illegal states unrepresentable. You define a type which contains a value between 0 and 1 (lets name it `probability`) and make a function `float -> probability` which checks the range. That way, everytime you'll see `probability` in your code, you will know it is in the right range.
The problem with spec is that it can only verify what it sees on run time, whereas a static type system by definition has 100% coverage over your entire program.
Compile-time and run-time floating point numbers constrained by precision and range. It's been a long time so I'm just going to include the examples in that document:
type Coefficient is digits 10 range -1.0 .. 1.0;
type Real is digits 8;
type Mass is digits 7 range 0.0 .. 1.0E35;
subtype Probability is Real range 0.0 .. 1.0;
I can't think of any typed language I've used or seen in active modern professional work where you could validate a value as part of a type at compile time.
https://docs.microsoft.com/en-us/dotnet/framework/debug-trac...
Yes and no, because nothing prevents you from passing the wrong kind of value in an untyped language unless, well, you check for the runtime type yourself in the function and reject that. And you can only do that at runtime, at which point you'll not be able to immediately see where you're passing in invalid data accidentally unless you hit this exact branch in your code. So actually just the type tagging is quite useful already.
Also, it looks like more powerful dependently-typed languages like Idris[0] (and probably also Agda and Coq) can encode this information in the type system.
Actually, it can, using dependent types :) I'm a Python fan, but Type-Driven Development with Idris has been a very interesting read.
I also wouldn't be surprised if Clojure tends to do surprising things in this area with taking Clojure.spec more to the compilation stage; some of the most interesting research into type systems has actually be done by lispers (i.e. Typed Racket, Core.Typed) and there is active interest in it among the Clojure community.
(For a number-type that is limited to eg be between 0.0 and 1.0):
Ada?
Sure, it can; many common numeric types include specific ranges, the fact that the range 0-1 doesn't match any common floating point type doesn't mean that it isn't one that could be a type.
Can you give me a mainstream language example?
Yes, it can! --- but you don't necessarily want to confound your program with such a thing.
The old adage about the cure being worse than the disease applies.
Ok, how? Other than an Ada example, or dependently-typed languages that aren't use in production, can you offer an example?
Every time someone gives you an answer, you modify the question to exclude it. Eventually you will have excluded everything that refutes the fallacy in your original post, but it is still there.
subset Positive of Int where * > -1
case class Probability(value: Double) { require(value <= 0 && value >= 1, "probability must be between 0 and 1" }I personally tend to do something much closer to TDD, and break my code out so I test each part with its own test rig. So I see when I do dumb things that need re-work. Again, typing is pretty much never an issue there.
While this is all anecdotal, I personally have found that enforcing boilerplate type defs actually increases my coding error rate. More LOC gives you more opportunities for errors.
FWIW, Julia (http://julialang.org) is IMO Python done right, and it is strongly typed. But done in such a way as to not actually get in your way most of the time. Like Python it has a great REPL, fantastic FFI, rapidly growing module list, very active development. Unlike Python, it has no issues with whitespace[1], is compiled (JIT for now, though static is planned from what I understand), is very fast, has multiple dispatch and a strong typing system.
The real point the article was making is, programmer time is the most valuable thing to optimize for. I completely agree with this, even though I disagree that Python is the right tool for (most) every job.
There are better tools IMO, which allow me to be far more productive, and spend as little time as possible on worrying about types ... which are rarely ever a concern for me.
I thought his comment about string processing was interesting, though he completely ignored Perl in the mix. I've found string processing in Perl to be almost trivial. Its harder (far more verbose boilerplate) in Python, and gets worse in other languages. Perl6 lets you embed grammars and write parsers without resorting to external modules (Marpa::* in Perl5). Takes building string processing, parsers, etc. to a whole new level, while making you even more productive.
But, as the author had noted, he is a pythonista. Everyone has their biases (including me). I want to code correctly quickly, and not have things that shouldn't get in my way, get in my way. Including type systems, massive boilerplate/odd syntax rules, etc.
[1] It is 2017 ... structure by indentation is somehow, still a thing. It shouldn't be IMO.
Yeah, C++ typing system sucks. Just don't think this generalizes to other languages.
Go: map[string]int64
Java: HashMap<String, long>
Rust: HashMap<&str, i64>
I think Haskell is one of the only statically typed languages which doesn't really care about algebraic typing. And yes, if you're talking about static typing, you get the baggage of dealing with algebraic typing to go with it as a rule. You can't arbitrarily separate the two until more languages follow Haskell's route.
OTOH, a language smart enough to (correctly) infer this (Perl, Julia, etc.) generally won't have a problem with this, and will handle these issues for you. Julia still allows you to be very explicit on type, and force a hard type specialized code. The benefit in this case, with type specialization, is that it can generate far more efficient code for the specific logic.
That latter argument is, to me, the only real benefit of typing systems that I've personally encountered. I know people throw studies around claiming "fewer errors with stronger type systems", but ... to be honest ... I have not experienced this. Rather, in stronger typed languages, I spend more time hunting down type impedance issues than logic issues.
This seems to not be a positive benefit to me. I may be alone in this regard, or not. I don't know.
I do know that, like programming languages, editors, operating systems, this view point (pro/anti strong typing) tends to take on a religious overtone in the sense of people taking a position and digging their heels in over this. Elevating this aspect as an important point in an overall platform decision process (what should we develop in), when, maybe, it shouldn't be.
In an odd way, I've seen this in the industry for a while. There were previous incarnations of this. Like Dijkstra's famous "goto" comments[1]. I don't necessarily agree with this, and I argue that people can write bad code in any language.
Typing systems ostensibly are there to help us write less bad code (all code is bad and buggy, anyone telling you otherwise is trying to sell you some swampland). But once they get in your way, and you start spending inordinate amounts of time dealing with typing issues, you have to ask whether or not they are helping or inhibiting.
Put another way, anything that helps should, actually help, without adding significantly to the burden. Apart from what Julia does, and other dynamic languages do ... that some people write great code in ... I've not seen/used many other systems that strive to get out of your way while working.
Typing systems do not automatically make code better. Absence of typing systems do not automatically make code worse. This is a function of the algorithm, the implementation logic, etc. How disciplined are you as the developer in making sure your code is clear, concise, and actually reflective of the problem you are attempting to solve ... things that help with that are welcome.
[1] http://homepages.cwi.nl/~storm/teaching/reader/Dijkstra68.pd...