Earlier quoted context omitted.
I'm reasonably convinced that once my program has passed the typechecker, it is logically correct Yup, this is one of my favorite things about Haskell, that's how I know that http://bpaste.net/show/32033/ is a totally correct program.
If you're hoping to catch a specification error, don't use a type like `Integer -> Integer`, which doesn't capture the specification except in a most general sense. Just as you should write good tests, that actually test for useful properties, so you should write good types -- and get useful proofs back from the compiler as a result.
Experiment: Unit testing isn't enough; You need static types, too
41–50 of 276 posts
Re: Experiment: Unit testing isn't enough; You need static types, too
#42Earlier quoted context omitted.
> Hindley-Milner type systems to the rescue! You're implying that all type-systems derived from HM have a form of bounded polymorphism. They're not, for example OCaml does not have type classes (you could probably encode a lot into objects, though).
False, ocaml has type classes now! (or maybe I'm thinking of coq)
I believe they're experimental in Coq.
Re: Experiment: Unit testing isn't enough; You need static types, too
#43 ( Bugs found by unit tests ( ) Bugs found by type-checking )
The disagreement is how much. Also, type-checking is free[1], while unit tests have to be manually written.I'm glad someone spent a lot of time trying to answer this question, but I don't think it will affect my choice of language in any new project. I like to write code in the languages I like, and bugs be damned.
1. A common argument is that static-typed languages slow development. I'm not touching that land-mine.
Re: Experiment: Unit testing isn't enough; You need static types, too
#44Earlier quoted context omitted.
From my personal experience, the saving in development time is very much real. I used to work on .NET, and you'd have to program against crazy, non-intuitive patterns in order to have your code "clean" (I hated IoC containers as well as writing all that boilerplate code for Attributes. And for Java, remember that hilarious post about Factory-Factory-Factory patterns http://discuss.joelonsoftware.com/default.asp?joel.…
The kinds of static type systems you find in C# & Java are too primitive. Something like Haskell with perhaps a little less religion about mutability is a whole different story.
Re: Experiment: Unit testing isn't enough; You need static types, too
#45Earlier quoted context omitted.
Haskell type classes are sufficiently flexible to represent things like 'does this type have a next method' without having to instrument the actual type.
But could that kind of type system be considered similar to the usual Java-like little-flexible static typing? I think I would prefer a static vs dynamic implemented as Java vs Python (since those are usually the subjects on every one of these discussions)
Re: Experiment: Unit testing isn't enough; You need static types, too
#46I think most people would agree that these two circles overlap on a Venn diagram: ( Bugs found by unit tests ( ) Bugs found by type-checking ) The disagreement is how much. Also, type-checking is free[1], while unit tests have to be manually written. I'm glad someone spent a lot of time trying to answer this question, but I don't think it will affect my choice of language in any new project. I like to write code in t…
Re: Experiment: Unit testing isn't enough; You need static types, too
#47How can you translate from python to a static language, when the code is written for the interfaces, and not types? How willl you translate a function receiving a (possibly custom) iterable, when the function doesn't care about the type, but just whether it implements a next() method?
Re: Experiment: Unit testing isn't enough; You need static types, too
#48In addition, the hidden assumption is that all static and dynamic typing are created equal, i.e., since Haskell is statically typed and Haskell appears to have caught Python bugs that unit tests did not, therefore Java will catch bugs in a Ruby codebase, C++ will catch bugs in a JavaScript codebase, etc. Of course this assumption is gratuitous. Haskell in particular has a specific sort of type checking that is far different from Java's or C++'s, for instance.
Further, not all dynamic systems are created equal. Ruby, for instance, I think can be shown to require fewer lines of code to achieve similar functionality to, for instance, Java. Fewer lines of code, should in principle mean fewer opportunities for defects. Dynamic languages with metaprogramming features like Ruby's or Smalltalk's should in principle be able to eliminate more code duplication than an environment like C++. This aspect of dynamic languages should be taken into account, again with a statistically significant sample size, and weighed against bugs caught by static typing.
The study is interesting as a preliminary investigation, but the conclusions should have been much more modest, proportionate to both the sample size, in terms of % of production codebases and the extremely important idiosyncratic nature of Haskell vs. other static typed environments. Something like: "The study has shown Haskell's type system will catch some bugs not caught in an otherwise well-covered Python codebase. These bugs could in theory have been caught by unit tests, therefore it is recommended that when using a dynamic language, more care must be taken to cover these types of bugs."
That would have been a more appropriate and modest conclusion, consistent with the data, than the sweeping generalization "You need Static Typing."
Re: Experiment: Unit testing isn't enough; You need static types, too
#49I'm convinced that dynamically typed languages are a transitional technology that will be superseded once we develop type systems that are both usefully strict but also flexible. After over ten years working in dynamic languages I'm very happy to have a compiler on my side again.
that's basically the design criteria behind Go's type system.
Re: Experiment: Unit testing isn't enough; You need static types, too
#50Interesting, but worth remembering, as Rich Hickey says, every bug has got past both your unit tests and your type checking.
Anyway, it occurred to me that with Clojure it could easily happen that I trade bugs caused by state problems to bugs cause by type problems.