[Haskell] Haddock, QuickCheck, and Functional Design by Contract
robertw at stud.tu-ilmenau.de
Tue Feb 17 10:50:30 EST 2004
> import QuickCheck
Dear developers of QuickCheck and Haddock,
((Summary: I'm trying to find notations for Design by Contract in Haskell
which can be standardised to be used by tools like Haddock and
QuickCheck. This will give Haskell programmers an order-of-magnitude
gain in productivity, since it brings semantic abstraction into the
programming language. See  and my earlier posts to this list .))
I consider it the most important advantage of Haddock, that it
encourages the separation of module internal and external
documentation (marked with -- | or -- ^). This is added value, even
if a module user only reads the source, not the generated
I consider it one of the most important advantanges of QuickCheck,
that it allows the automatic verification of (formal) documentation,
namely algebraic properties of functions. Yes, I think that that
(well-written) QuickCheck properties are excellent documentation, much
more worth than just type signatures (which I can look at in the
I consider it the essence of Design by Contract to have an explicit
redundancy in the code, namely Pre- and Post-Conditions, Assertions,
whose consistency with the rest of the code is automatically checked
during run-time, making it a tight net in which bugs are caught. And
what's more, this redundant view is more abstract than the original
code, so that it makes for excellent documentation, which can never be
out of date (due to the run-time checks).
Both the principles "Only one document for code and documentation" and
"Contracts have to be run-time checked" were already articulated in
1988 . A standarised notation for contracts should therefore be
part of any programming language. The following six points summarise
a functional version of Design by Contract. Point 4 is still unclear,
others can still change syntax. The rest is relatively straight-
forward and we should make it a standard as soon as possible.
1. A notation for postconditions: No problem, use QuickCheck
> prop_sort_post xs = let xs' = sort xs
> in is_sorted xs' && bag xs == bag xs'
- Haddock can automatically include this "postcondition" in the
documentation for function @sort@ (removing the prefix "prop_"
and the suffix "_post" from the QuickCheck-Property).
- For QuickCheck it is already in the right format.
2. A notation for specificative functions. That is, we document /
specify a function by giving a more readable (but less efficient)
version with the same semantics.
For example, the best way to document exponentiation (besides the
informal "@x ^ n@ is the @n at th power of @x at .") is the following
> x ^ 0 = 1
> x ^ n = x * x^(n-1)
Or the standard function @scanl@ is specified as
> scanl f e = map (foldl f e) . inits
> -- @inits@ see appendix.
Both of those definitions are not the actual implementation (which
is asymptotically faster in both cases), but they are perfectly
suited for inclusion in the documentation and as raw material for
QuickCheck. We can realise that by a simple notation:
> scanl_spec f e = map (foldl f e) . inits
Haddock would then publish the definition @scanl f e = ..@
(i.e. with the suffix "_spec" removed) in the documentation.
QuickCheck would generate the testing property:
prop_scanl_spec f e = scanl f e == scanl_spec f e
The same can be done for functions with operator names, e.g. with
"//" as suffix for the specification function and "\\" as prefix in
x \\^// n = x ^ n == x ^// n
(We could also generate names, like "roof_spec" and
"prop_roof_spec" for use in the code. The documentation, however,
will only show the clear @x ^ n at .)
3. A notation to mark self-specifying functions. These are functions
where the implementation is at the same time the simplest (still
For example the function @square@ from the Haddock manual:
square x = x * x -- ||
The double bar tells Haddock to export the complete function
definition to the user documentation. Another example comes from
(<>) = append -- || Only syntactic sugar.
lookup k map | member k map = Just (find k map) -- ||
| otherwise = Nothing -- ||
-- | Perhaps implement more efficiently later.
The documentation that contains those defintions does not reveal
whether the functions are really implemented as given, or whether
it's only a specificative functions according to point 2. However,
since point 2 guarantees semantic equivalence through tests, users
don't need to care.
For many people self-specifying code seems to be opposed to design
by contract, however, this is not at all the case. The modern view
of Programming by Refinement (see, e.g. ) softens the frontier
between specifications and implementations to allow practical
compromises between readability and efficiency while at the same
time avoiding negative redundancy between code and spec
(i.e. simply duplicated information instead of a useful different
view). Incidentally most of the Prelude functions are self-
specifying in this way. The examples of point 2 are notable
4. A notation for preconditions. For simple functions a Precondition
can be calculated automatically from the Patterns:
> head (x:xs) = x
Gives the Precondition @xs /= @ for @head xs at . This only needs
some simple knowledge about @data@ and @newtype@ declarations. (We
could also choose to leave it out, if it's too much work, for too
few cases where it works. Then programmers would have to state all
preconditions explicitly as shown next.)
Presently I use the following coding style:
> take n xs | not (n >= 9) = error "take.Precondition"
The precondition can simply be extracted as <<the bracketed
expression behind @not@ in a line containing the words @error@ and
However it has the disadvantage that I can't simply disable
run-time checking of the Precondition (as I could when using
@assert@). Furthermore it is also rather ugly. Does anyone have a
The use of Preconditions is expecially important:
- Automatically checked on run-time (like @assert@).
- Used in documentation.
- Used by QuickCheck to create (==>) guards in the automatic
5. Default implementations of type class members are often a special
case of specification functions: the overwriting provides the same
semantics, more efficiently. (Occurs often in Abstract Data
Structures, see .)
A typical example is:
> is_empty coll = size coll == 0 -- ||
We can use the double bar (or whatever we decide to standardise),
to mark the function definition for export to the documentation.
However, it is more difficult to create test properties which
compare the two implementations of a function, since the default
implementation is no more accessible after having been overwritten.
The property generator will have to copy the default definition to
a definition with name @is_empty_spec@ (for example) and can then
generate the usual @prop_is_empty_spec@ (as in point 2). The
copying of the function definition happens only for testing and is
not seen in normal code or documentation.
(The overwriting corresponds slightly to the contract refinement in
object-oriented inheritance. See .)
By the way, we can use -- || on a type class header, saying to
export all it't default definitions to the documentation. (In my
data structure library this is always the case. See, e.g.,
6. Invariants are an important part of Design by Contract according to
In Functional Programming it has been proven practical to check
(and at the same time: document) data structure invariants in a
smart constructor; the invariant resides only in this place (is
not redundantly mentioned in the code) and is run-time checked on
each creation of a data cell. This works with @assert@ and doesn't
need QuickCheck properties. Also, such internal invariants are not
relevant for the external documentation. (Otherwise we could
documentation- export the definition of the smart constructor,
using -- ||.)
External Invariants are nothing else than algebraic properties of
data structures. They can be documented using normal QuickCheck-
Properties, and these can be documentation- exported via -- ||.
As a consequence, invariants need no special notation. I only
mention them her for methodological reasons.
In order to keep the standard short, I suggest only to include this
notations, the discrimination between internal and external comments
(as in Haddock) and the discrimination of identifiers in comments
(also editors can have hyperlinking and different colors.) Further
markup concerns only the documentation generator and not other tools.
Users of QuickCheck have reported an order-of-magnitude gain in
productivity. That's because redundancy in form of checkable
documentation comes very near to semantically automated software
engineering. Together with proper documentation mechanisms, we can
make such rendundant programming more literate, thus bringing an
order-of-magnitude gain in productivity to whole programmer _teams_.
Finally, I think, that the topic "Functional Programming and Design by
Contract" is also a topic for a keynote lecture. Those who are in the
relevant positions might about that. Similar applies to the authors
of functional programming text books (and teachers, by the way). Or,
and fans of program proving (hello LARCH and OBJ2) might want to
statically check those contracts...
"Modularity without Abstraction is no more than Syntactic Sugar"
 myself: "Posts on Functional Data Structures"
 Bertrand Meyer: "Object-Oriented Software Construction", 1st
 Richard Bird: "Introduction to Functional Programming using
Haskell", 2nd ed.
 Eric Hehner: "A Practical Theory for Programming", 2nd ed., 2004
> -- | List of initial segments (including ) of a list
> -- in increasing order of size.
> inits  = []
> inits (x:xs) =  :
> map (x:) (inits xs)
> prop_inits_initial xs = forAll (elements $ inits xs) (\ ys ->
> ys == take (length ys) xs )
> prop_inits_increasing_length xs
> = striclty_increasing $ map length $ inits xs
> -- Also checks, that no segment occurs twice.
More information about the Haskell