[Haskell-cafe] Type System vs Test Driven Development

[Florian Weimer]

* Jonathan Geddes:

> When I write Haskell code, I write functions (and monadic actions)
> that are either a) so trivial that writing any kind of unit/property
> test seems silly, or are b) composed of other trivial functions using
> equally-trivial combinators.

You can write in this style in any language which has good support for
functional composition (which means some sort of garbage collection
and perhaps closures, but strong support for higher-order functions is
probably not so important).  But this doesn't mean that you don't have
bugs.  There are a few error patterns I've seen when following this
style (albeit not in Haskell):

While traversing a data structure (or parsing some input), you fail to
make progress and end up in an infinite loop.

You confuse right and left (or swap two parameters of the same type),
leading to wrong results.

All the usual stuff about border conditions still applies.

Input and output is more often untyped than typed.  Typos in magic
string constants (such as SQL statements) happen frequently.

Therefore, I think that you cannot really avoid extensive testing for
a large class of programming tasks.

> I vehemently disagreed, stating that invariants embedded in the type
> system are stronger than any other form of assuring correctness I know
> of.

But there are very interesting invariants you cannot easily express in
the type system, such as "this list is of finite length".  It also
seems to me that most Haskell programmers do not bother to turn the
typechecker into some sort of proof checker.  (Just pick a few
standard data structures on hackage and see if they perform such
encoding. 8-)