Live data from Hacker News

Type Wars

blog.cleancoder.com

41–50 of 62 posts

Re: Type Wars

#41

Earlier quoted context omitted.

Exactly. Types are a class of tests, checked by the compiler at compile time.

Right. They are one class of tests that happens to be checked at compile time. But what about all the other tests that you still have to do? Which typically also coincidentally check the types (if I check that a value is > 2, I am also checking that its type is number (or int or whatever your particular numeric tower or non-tower says). And what is the value of "compile time", if the all this type checking makes the…

>if I check that a value is > 2, I am also checking that its type is number

Surely, you're only testing that it can be coerced to a number?

Re: Type Wars

#42

Ruby salaries tend to be higher than JVM salaries? What?

I was surprised by that statement too, I don't think it is true in London.

Really? My experience is that while there are a number of high-end Java positions, and a number of Ruby positions in well-funded startups and such, there are VAST numbers of Java positions for mediocre engineers and mediocre companies – no fault of the language, more of the niche it has found itself in. I'm not surprised at all to find that this drags the average salary down.

Re: Type Wars

#43

Earlier quoted context omitted.

>Tests are not proofs Neither is static typing. It's a layer of protection, much like tests. >Tests are more work I don't think that's necessarily true. You still need to write tests with or without static typing. Those tests you need to write anyway will usually catch type errors in a dynamically typed language that a statically typed language picks up at compile time. The question is whether you need to write more…

>Tests are not proofs Neither is static typing. It's a layer of protection, much like tests. Proofs are exactly what the results of strong static type systems give you. They can't prove everything , but they do prove certain things in all possible cases.

If you are willing to adopt a strong enough type system pretty much any interesting property about a program you want to prove is provable. Its just a matter of ergonomics, more complex type systems provide power, but require investment in understanding, both conceptually, and in modeling your problem.

You can also adopt automated verification techniques that can prove strong properties about a system automatically.

Re: Type Wars

#44

Earlier quoted context omitted.

>Tests are not proofs Neither is static typing. It's a layer of protection, much like tests. >Tests are more work I don't think that's necessarily true. You still need to write tests with or without static typing. Those tests you need to write anyway will usually catch type errors in a dynamically typed language that a statically typed language picks up at compile time. The question is whether you need to write more…

>Tests are not proofs Neither is static typing. It's a layer of protection, much like tests. Proofs are exactly what the results of strong static type systems give you. They can't prove everything , but they do prove certain things in all possible cases.

>They can't prove everything, but they do prove certain things

Much like tests then?

Re: Type Wars

#45
Modern type systems made type inference and gradual typing possible and those are making a huge difference nowadays.

With type inference you can write programs almost as easily and productively as in dynamic languages. With gradual typing you can basically write the same code as in a dynamic language and still get type safety (e.g. TypeScript).

Swift, Go, (Rust, Scala, C# etc. but even C++) has type inference today. Maybe dynamic languages will get type annotations and gradual typing in the future and then basically we can have the best of both worlds.

Re: Type Wars

#46

> My own prediction is that TDD is the deciding factor. If this turns out to be the case, then people would reach for statically typed languages to augment & cut-down on tests. Like everyone here is saying, the pendulum is moving toward statically typed. The next generation will probably be in higher kinded types as we continue to attempt to write more generic code that cuts down on number of lines, but still preserv…

"Clever" or "overly specialized", depending on your viewpoint.

I think they made a much better decision then everyone else even if verbose.

Nearly every language has continued to repeat Tony Hoare's "billion dollar" mistake of allowing null to inhabit any type. I think approaches like Rust's and Swift's are steps to stamp out something that never should of existed in the first place.

Re: Type Wars

#47
While it might seem like things are shifting back towards static typing, I think that is primarily happening in the development of technology now but not the use of that technology yet. I think these predictions will probably appear to be true for some period of time before these newer typed languages begin to gain larger amounts of usage. (However, I expect the testing will probably stick around. I'm highly skeptical of the idea that typing and testing are some how interchangeable.)

Also, I think it'll be interesting to see what role gradual typing systems like Flow, Hack, and TypeScript might have on getting static typing into existing dynamically typed codebases.

Re: Type Wars

#48

Earlier quoted context omitted.

Good point, the author clearly misses the point that tests themselves are code and thus can have errors in them as well. Code coverage is just a vanity metric if you're tests don't actually test the correct thing.

Types are also code and can have errors in them...

Types aren't code.

Re: Type Wars

#49

Earlier quoted context omitted.

>Tests are not proofs Neither is static typing. It's a layer of protection, much like tests. >Tests are more work I don't think that's necessarily true. You still need to write tests with or without static typing. Those tests you need to write anyway will usually catch type errors in a dynamically typed language that a statically typed language picks up at compile time. The question is whether you need to write more…

> Neither is static typing. It's a layer of protection, much like tests. Not true. The curry-howard correspondence shows the relationship between typed programs and proofs. I recommend you watch a Phillip Wadler talk about this: https://www.youtube.com/watch?v=aeRVdYN6fE8 Note: This doesn't mean that type systems can prove _all assertions_ about a program, but type systems do indeed work as provers. > I don't think t…

>Note: This doesn't mean that type systems can prove _all assertions_ about a program, but type systems do indeed work as provers.

Type systems can verify certain properties about code much like a test does, but that's far from being a mathematical proof of program correctness (especially since compilers have, you know, bugs).

>This isn't necessarily true unless you test for all inputs (which tends to be infeasible in most cases).

No, it's necessarily true. The vast majority of type errors I experience get picked up during TDD. A small minority reach production.

It's very easy these days to write tests that cover an enormous range of inputs and outputs (e.g. see quickcheck).

I'd estimate that maybe 5% of errors I experience in production are type related (in a dynamically typed language). That's offset against quicker development time (which also eans ease of fixing the other 95%).

>I believe there is almost no overhead imposed by a static type system

I think that's wishful thinking.

>In practice I've never had a bug with the type system (that I'm aware of)

Which type system have you never had a bug with? I've dealt with several buggy, crappy type systems?

>In practice I've never had a bug with the type system

I've seen plenty of bugs caused by picking the wrong type.

>I've seen hundreds of bugs from incorrect test assertions.

So have I. Different types of bugs though. The kind which static typing doesn't help eliminate.

Re: Type Wars

#50

Earlier quoted context omitted.

Exactly. Types are a class of tests, checked by the compiler at compile time.

Right. They are one class of tests that happens to be checked at compile time. But what about all the other tests that you still have to do? Which typically also coincidentally check the types (if I check that a value is > 2, I am also checking that its type is number (or int or whatever your particular numeric tower or non-tower says). And what is the value of "compile time", if the all this type checking makes the…

> But what about all the other tests that you still have to do?

You should do those too.

> Which typically also coincidentally check the types (if I check that a value is > 2, I am also checking that its type is number

    ~$ python -c 'print "foo" > 2'
    True
Now, on the bright side, Python 3 fixes that one:

    ~$ python3 -c 'print(2 ", line 1, in 
    TypeError: unorderable types: int() 
But most popular dynamic languages seem to have more where that came from. And if you have a sufficiently robust type system not to, then it starts to look a lot like the type system of a static language, minus the compile-time error detection.

> what is the value of "compile time", if the all this type checking makes the compiler so slow that just compiling is slower than compiling + running unit tests in a simpler language?

To the best of my knowledge, type checking is hardly the slowest part of most compilers. Many dynamic languages have somewhat faster startup times because they don't have a compiler, or they use a JIT at runtime. In any case, for many non-trivial programs, runtime dominates. A sufficiently thorough unit test suite may take significantly longer than compilation. And even if not, someone has to write the unit tests that handle what static type checking does for free.

I'm not going to claim that static typing is universally better; for instance, it's a lot harder to provide a good REPL in a statically typed language. But personally, I like dealing with as many errors as possible up front, rather than discovering them later on.

Post reply on HN