Live data from Hacker News

Type Wars

blog.cleancoder.com

51–60 of 62 posts

Re: Type Wars

#51
post #3

> Why am I wasting time satisfying the type constraints of Java when my unit tests are already checking everything? Couldn't you invert the question for Java and instead ask, why am I wasting my time chasing 100% test coverage when the type constraints of the language guarantee a certain degree of correctness? I've always found that dynamic language projects require twice as many tests as a Java project to get a simi…

Also, how does full unit (!) test coverage prevent a situation where unit A passes some type to unit B that unit B doesn't expect but happily runs with, but with different semantics?

Documentation of interfaces in dynamic languages usually always specify the types of arguments and return values, and the code very often looks like this:

    def foo(arg)
      raise TypeError, "Integer argument expected" unless arg.kind_of?(Integer)
      # ...
    end
Yup. That saved me a lot of typing (no pun intended) compared to

    void foo(int arg) {
       // ...
    }
Reading (and writing) code in dynamic languages (including the tests!) always seems to me to disprove all of their purported benefits and underlines the need for a strong type system.

Re: Type Wars

#52

Earlier quoted context omitted.

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

Tests actually prove very little. They probe the code with a few, isolated inputs out of a usually very large domain. Their nature is more stochastic.

Static type guarantees are actual proofs (barring a compiler bug), and they narrow down the domain that your tests have to probe.

Re: Type Wars

#53
post #36

Earlier quoted context omitted.

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…

Don't underestimate the productivity boost provided by the little squiggly red line. The fact that your tooling will stop you from ever passing T when the expected parameter is Collection , and that this "rescue" involves pretty much zero cognitive overhead, is invaluable. When I work in a statically typed language, I find that I pretty much never make "head-desk" type errors, and despair at their reappearance when w…

Hmm...much of the disconnect might be that when people think "dynamically typed language", they think JavaScript and Python and Ruby.

I also don't make these mistakes while writing Smalltalk.

Re: Type Wars

#54
post #3

> Why am I wasting time satisfying the type constraints of Java when my unit tests are already checking everything? Couldn't you invert the question for Java and instead ask, why am I wasting my time chasing 100% test coverage when the type constraints of the language guarantee a certain degree of correctness? I've always found that dynamic language projects require twice as many tests as a Java project to get a simi…

Also, how does full unit (!) test coverage prevent a situation where unit A passes some type to unit B that unit B doesn't expect but happily runs with, but with different semantics? Documentation of interfaces in dynamic languages usually always specify the types of arguments and return values, and the code very often looks like this: def foo(arg) raise TypeError, "Integer argument expected" unless arg.kind_of?(Inte…

Yup, the right tool for the job. Type systems are really good at enforcing inter-unit contracts, while tests (especially property tests) are very good at making sure that the implementation is correct for at least a subset of inputs.

Re: Type Wars

#55

Earlier quoted context omitted.

> 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 i…

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

I'm not trying to argue against your experience (or persuade you against it, for that matter). Only making a point that it is possible for you to have type errors that go uncaught by unit tests unless (unless you run those tests against all values).

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

Quickcheck takes advantage of types to narrow the inputs for generative tests, whereas dynamic languages have to content with any possible input.

>> I believe there is almost no overhead imposed by a static type system > I think that's wishful thinking.

Here's a couple ways I think you actually waste more time in dynamic languages:

1. Type checks. Sounds almost tautological, but it's true. Any time you see someone using the type() function in python, you're branching in code for something a compiler could take care of for you.

2. Redundant validation, specifically against a purely functional language that is statically typed. Since types encode facts about data and functions encode theorems, statically typed languages only require one test to verify the assumptions in a theorem. In other words, if there is one function creating values of type Foo with an integer attribute "foo" and it insures that "foo" is 0, I never need to check if foo is 0 anywhere in production code. I only need to check that in a single test of the constructor. In practice I find this means I need to write a lot less tests with a statically typed language, and generally a lot less branches in code.

3. Documentation comprehension. I can't count the number of times I've read a javascript library's documentation only to be thoroughly confused about what kinds of values can be passed to a function legally. Since the language provides no way to enforce this, it seems to encourage a culture of negligence about documenting what invariants of data are required to hold. Furthermore I rarely get a descriptive exception informing me what the issue is, rather I get a type error about a missing attribute or something.

4: Boilerplate code. Fixed data schemas mean you can generate efficiently executing code to perform tasks like serialization, client libraries, etc. Take a look at servant: https://haskell-servant.github.io/ Because haskell is statically typed, the type system makes it trivial to generate an HTTP server, a client, and a swagger API docs page all from a couple types. This can be done for certain things in dynamic languages, but since it requires introspection it will almost definitely be slower (and in some cases that may make it impractical to use).

5. Refactoring. Dynamic types are notoriously a pain for editors. Values can be changed ad hoc in ways that make it very difficult to change names without some smart regexes. Refactoring in statically typed languages is a breeze with a sufficiently smart editor/ide. Find and replace is generally two clicks away and is guaranteed to find all occurrences and replace them safely.

6. Condition checking. Pattern matching is not exclusive to statically typed languages, but it is much more common in them. Static type systems also allow for exhaustivity checks that a dynamically typed language cannot perform.

In general I think the things people claim are time consuming about statically typed languages are based on older languages that are lacking richer type system features. Things like:

1. Omnipresent type annotations. In haskell you almost never have to specify one of these (in fact you can get near 0% of these if you turn off the monomorphism restriction). The most common use of type annotations in for function signatures, which I find are nice to have for documentation purposes anyways.

2. Inability to perform generalizable code. A lot of people base this on experience with languages like Java, which is unfortunate because the state of the art is much farther ahead. There are many "dynamic feeling" generalizations you can get out of newer statically typed languages. For instance, you can easily generate a "falesy" abstraction similar to python or javascript through haskell typeclasses. Typeclasses, functors, etc. are all examples of statically typed features that allow you to write abstract code over disparate sets of types.

Re: Type Wars

#56
post #36

Earlier quoted context omitted.

Don't underestimate the productivity boost provided by the little squiggly red line. The fact that your tooling will stop you from ever passing T when the expected parameter is Collection , and that this "rescue" involves pretty much zero cognitive overhead, is invaluable. When I work in a statically typed language, I find that I pretty much never make "head-desk" type errors, and despair at their reappearance when w…

Hmm...much of the disconnect might be that when people think "dynamically typed language", they think JavaScript and Python and Ruby. I also don't make these mistakes while writing Smalltalk.

What feature of Smalltalk, but absent in Python/Ruby/JS, prevents these mistakes?

Re: Type Wars

#57
post #46

Earlier quoted context omitted.

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

> Nearly every language has continued to repeat Tony Hoare's "billion dollar" mistake of allowing null to inhabit any type.

Perhaps I was unclear. I could not agree more with this assessment (see link to my blog post in sibling).

I was merely commenting on Swift's choice to do it in a (to quote the OP) "clever" way, rather than a general one like Rust or Scala.

Re: Type Wars

#58
post #43

Earlier quoted context omitted.

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

All true, up to a point at least. Strong, static type systems aren't universal wins with no drawbacks.

However, I think it's fair to say that even the "strongish, staticish" type systems in a lot of mainstream languages can still prove very useful properties that are often sources of bugs in the more dynamic languages. A good example would be not accidentally allowing null values to be passed around, as mentioned elsewhere in this discussion. And of course some of less well known but still not uncommon languages, such as the popular functional programming choices or newer offerings like Rust, can do quite a lot more without their type systems becoming an unreasonable burden.

Re: Type Wars

#59

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

I see this argument from fans of dynamic typing quite a bit. Gary Bernhardt manages to defeat it better in 5 minutes than I could in a lifetime, so here you go:

https://www.destroyallsoftware.com/talks/wat

Re: Type Wars

#60
post #12

> The language is very opinionated about type safety... For example, the fact that a variable of type X might also be nil means you must declare that variable to hold an "optional" value... The extreme nature of the type system in swift Oh boy, if he thinks that's extreme... > Why am I wasting time satisfying the type constraints of Java when my unit tests are already checking everything? Oh really? Are the unit test…

> Are the unit tests testing every single 2^64 possible values of an Int? Hmm...your usual type checker is checking 0 possible values of an int. It is checking just the type. And of course if you are checking a value in a test, you ar coincidentally also checking its type. That's not to say that types can't be useful (for example they have been shown to be quite useful as machine-checked documentation for getting aro…

In fact, it checks every predicate codified by the type system. The question is how powerful your type system is, because this determines what predicates you can (conveniently) test.

Well-designed strongly typed languages naturally check some useful predicates (existence, the exact structure of the value, etc.). These alone are sufficient to eliminate null pointers, non-total functions, and most other failure modes that plague languages like C++ or Python.

Stepping it up a notch, you can use things like GADTs and kind promotion to check much more advanced predicates (like that a vector must be non-empty or even length).

With refinement types a la liquid Haskell, I can statically guarantee that e.g. my function only returns lists of even length or only returns even numbers, without even having to put this information in the type of the returned value.

With full-blown dependent types a la Coq/Idris/Agda, you can encode pretty much whatever property you want into types. For example, Idris has `verifiedMonoid` which statically guarantees that an operation is associative and has an identity. See https://github.com/idris-lang/Idris-dev/blob/master/libs/con...

Post reply on HN