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


_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Reply via email to