(I would have used the "Reply" button, but I don't have permission.
Ref: http://www.cs.chalmers.se/~rjmh/Haskell/Messages/Display.cgi?id=290)

In general assertions provide two useful services:
* they help the programmer find bugs and document assumptions within code
* they aid in code reuse by specifying the contractual commitments between
        modules

The proposal to which you link helps somewhat with the former (no
invariants on datatypes), but not really the latter. (otherwise you would
be able to attach assertions to classes).

At a minimum, it would be a little nicer if the programmer
could add an optional message to assertions e.g.

> f xs ys = assert (length xs == length ys) $ --! lengths must match
>                 ...rest of code for f...

if the condition is violated then the message is:

"Assertion failed on line 32 of Foo.hs -- lengths must match".

Also, assertions violations should raise an exception not return BOTTOM.
(I didn't see exceptions on this list, are they a 2.0 or 1.4 feature?)
--
However, in my general campaign for more support for programming in the
large and because contracts are so important in that context, I would like
Haskell add real Eiffel style assertions.
(see Building bug-free O-O software: An introduction to Design by Contract
      http://www.eiffel.com/doc/manuals/technology/contract/index.html)

Eiffel assertions are more like a part of a function's signature than its
implementation.  Meyer argues that you need to know the contractual
commitments of a function in order to use it, but you don't need to know
its implementation.  For example, you may want to specify not only that
instances of a class match a particular signature, but also that they
fulfill certain preconditions/postconditions.

In Haskell, it is really hard to know what a function does without looking
at its implementation because Haskell signatures don't allow the
programmer to communicate enough.

Users should have the options of:
* putting variable names in type signatures  (using @ perhaps)
* specifying pre/post conditions in signatures rather than in code
* attaching keywords and descriptions to functions in a standard way for
        generating library documentation

I imagine this would look something like:

> functionName:: x@a -> y@b -> z@c  -- a,b,c are types x,y,z are arg names
>   --keywords: sorting searching facilitating
>   --description: functionName does something with x and y
>   require 
>       foo x==goo y --! arguments must have foo/goo correspondence
>       blah x       --! x must be blah
>   ensure 
>       blah2 z 2.0  --! functionName violated blah2 condition
>   where blah2 x y = foo x == foo' y 

It would also be useful to have the same features in data types a.k.a.
invariants.

> data OrderTree a= 
>  Leaf value@a 
>    invariant
>       blah value  --! leaf values must satisfy blah
>  Node value@a left@(Tree a) right@(Tree a)
>     invariant 
>       left `lessthan` right --! left must be lessthan right
>  where
>   lessthan x y = ....

Invariants are useful both for debugging and reusability.
(Note this abandons the | syntax in favor of a layout rule)

I don't know how hard this would be to implement, but it will make life
much nicer when Haskell implements a binary linking standard and people
want to create large libraries.

-Alex-
___________________________________________________________________
S. Alexander Jacobson                   i2x Media  
1-212-697-0184 voice                    1-212-697-1427 fax










Reply via email to