[nightski]

Doesn't anyone view static typing as done in a language like Haskell as a form of documentation? I am not saying ALL Haskell code can be deciphered by its types - hell no. But a useful technique is to express the semantics of the program into the type system (as much as possible anyways) to communicate intent. This is a huge benefit over dynamic languages imho. So there is more too it than just verification, even if that is extremely nice.

[tikhonj]

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.

[gtani]

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.

[stonemetal]

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.