[Haskell-cafe] Type System vs Test Driven Development

[Heinrich Apfelmus]

Florian Weimer wrote:
> * 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):

As you mention, the bugs below can all be avoided in Haskell by using 
the type system and the right abstractions and combinators. You can't 
put everything in the type system - at some point, you do have to write 
actual code - but you can isolate potential bugs to the point that their 
correctness becomes obvious.

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

Remedy: favor higher-order combinators like  fold  and  map  over 
primitive recursion.

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

Remedy: use more descriptive types, for instance by putting  Int  into 
an appropriate newtype. Use infix notation  source `link` target.

> All the usual stuff about border conditions still applies.

Partial remedy: choose natural boundary conditions, for example  and [] 
= True,  or [] = False.

But I would agree that this is one of the main use cases for QuickCheck.

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

Remedy: write magic string only once. Put them in a type-safe combinator 
library.

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

Hopefully, the class is not so large anymore. ;)

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

Sure, you can.

    data FiniteList   a = Nil | Cons a !(FiniteList a)

I never needed to know whether a list is finite, though. It is more 
interesting to know whether a list is infinite.

    data InfiniteList a = a :> InfiniteList a

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

I at least regularly encode properties in the types, even if it's only a 
type synonym. I also try to avoid classes of bugs by "making them 
obvious", i.e. organizing my code in such a way that correctness becomes 
obvious.


Regards,
Heinrich Apfelmus

--
http://apfelmus.nfshost.com