Static Typing is not enough (opens in new tab)

QuickCheck is great and can be found in many languages - dynamic and static alike - nowadays. Another tool that is currently unique to Haskell and is easier to write tests for is Lazy/SmallCheck. SmallCheck shines in the left long tail of failure. Its core idea is based on a powerful principle: "If a program does not fail in any simple case, it hardly ever fails in any case."[]

So SmallCheck works exhaustively to find a minimal counterexample within some depth bound. This makes sense - when trying to characterize a structure for failure (or anything) you can rarely do better than the simplest explanation. However, when the problem lies in larger examples SmallCheck fails where QuickCheck catches a result so something like Type Check -> SmallCheck -> QuickCheck -> probably ok.

[] http://www.cs.york.ac.uk/fp/smallcheck/ documentation

This is actually a rather underrated property of good static type systems. Some types (like (a, b) -> a or a -> b -> a) are actually so constraining, they can only have one valid (e.g. not ⊥) implementation. There is actually a program that, given a type signature, can write the trivial function for you [1]. It's pretty awesome, but admittedly more a curio than anything practical.

[1]: http://lambda-the-ultimate.org/node/1178

Happily, there are practical programs that take advantage of the types' expressiveness. My favorite example: Hoogle[2]. It's brilliant: a search engine that given a type signature gives you a list of functions either with that type (modulo renaming) or a similar type. The beauty is that it can work even if the function is more general than what you're looking for and has a weird name (so a normal search would not be very helpful).

[2]: http://www.haskell.org/hoogle/

A perfect example: let's say you're looking for the equivalent of JavaScript's join method. It would have the type [String] -> String -> String. Now, this particular function does not actually exist in Haskell. Instead, there is a more general function called intercalate that works on any list. Moreover, intercalate's arguments are reversed: it's type is actually [a] -> [[a]] -> [a] (or String -> [String] -> String if made specific to String). And yet, if you search for [String] -> String -> String, the second result is intercalate! It's magical.

In short: types are basically a form of self-documenting code, so you get a lot of cool stuff for free given a good type system.

GHC/Haskell is edging towards what could be called weak dependent typing or type-level programming, look at Weirich deck and phantom types:

http://www.cis.upenn.edu/~sweirich/plmw12/Slides/plmw12-Pier...

http://www.haskell.org/haskellwiki/Phantom_type

http://stackoverflow.com/questions/8600692/datatype-promotio...

For scala:

http://groups.google.com/group/scala-internals/browse_frm/th...

http://www.chuusai.com/2012/01/27/type-level-sorting-in-shap...

-------------

SAT and SMT solvers, e.g. in OCaml

http://caml.inria.fr/cgi-bin/hump.cgi?contrib=706

-----------------

I could give a few dozen more examples in these 3 languages, incluindg Coq which is written in C and OCaml, and agda and idris and others, which are written in C and haskell, or compile down to some stage of haskell compilation.

In some way yes, but in general not really.

(+),(-), (*) all have the type (Num a) a -> a -> a

abs, signum both have the type (Num a) a-> a

In the first case it works as documentation because I already know what they do. In the second case I read signum as sig num instead of sign num, and was left scratching my head as to what a signature number was, until I read the actual documentation.

So I would say types make a good reference documentation but not a good learning documentation. Contrast this with python doc strings which can be both a good reference and a decent source of learning.

    (any of the other stuff mentioned) .. ensure correctness

The post says that.

Dot-completion in your IDE is not enough either, nor is it something particularly unique to static languages.

It's a response to a previous article, which really did make the argument "unit testing does not guarantee quality, therefore you need static typing". So not a strawman.

Yes, but perhaps we it means we can stop bitching about each other's bullets of choice and get back to shooting.

I'm question if you read the post because I didn't diminish anything. I did say that it is a tool in the fight of software validation however.

Yes, exactly. The author didn't like the original article and decided to throw around some strawmen.

There might be something to that. But maybe some construction and automobile engineers feel the same way about bridges and cars respectively. God, I hope not. :)

The first half is a bit easier - if you can show some implementation meets the specification it is at least consistent.

The second isn't so clear, but sometimes you can get a bit more confidence by showing that other good properties are implied by the specification alone.

With appropriate compiler flags, you can make up any sort of contracts you like in Haskell. But there's no guarantee that the compilation process will terminate if you do, even putting aside the impenetrability of the resulting code. Haskell is not a general purpose proof assistant, and the typing definitely has limits both practical and theoretical. Abstractly, static types can represent anything, however we (by which I mean humanity in general) certainly do not know how to use such powerful types in real, general purpose code.

If you want to go that road, look up Agda or Coq.

    Haskell's type system is Turing-complete

So? What does that buy you in the face of attempting to prove that your system can run with two simultaneous users? How does the type system prove that it can withstand a DoS attack? Likewise, how can it prove that your system properly handles the case where the user types some garbage into a textbox? How does it help prove that your system keeps running if someone pulls the network cable out of the wall? How does it help prove that you wrote the system that your client wanted?

Incorrect. Haskell's type system cannot ensure arbitrary correctness guarantees. Hence the research into dependently typed languages, like Agda and Coq.