On Thu, 16 Apr 1998, Simon L Peyton Jones wrote:
> > 2. how would I have found/fixed such an error in a more complex function
> > w/o assertions and w/o print statements?
>
> Good questions
>
> There was a proposal to put assertions into Std Haskell, which we
> have implemented in GHC. (I'm not sure we've yet put that version out
> though.) So assertions are definitely coming. You are right that they
> are important.
Not to reject assertions (they would be welcome), but I think that you
need something slightly different in a functional programming language.
Assertions in procedural languages typically define system state before
and after a particular function gets executed.
State assertions are less appropriate to functional programming languages
(except in the context of the content of monads but that is a separate
issue). As I understand it, Haskell programmers should use the type system to prevent
functions from getting called w/ operands outside their domain.
For example, a very careful programmer would specify that division is only
allowed on a type that has already filtered out 0
e.g.
> newType NonZero :: MakeNonZero Num
> toNonZero:: Num -> NonZero
> toNonZero x | x==0 = error "Shouldn't be zero"
> | otherwise = MakeNonZero x
Another application of assertions is documenting and formalizing the spec
for functions. In this context assertions may provide a way of documenting
code with a proof-of-correctness but this is of limited utility. In many
contexts the risk that the spec is incorrect substantially outweighs the risk
that the code is incorrect (and even more so in a functional programming
language).
All that being said, we can say that there are certain properties that
all haskell functions must fulfill. For example a recursive function
should never call itself with the arguments that it recieved.
e.g. myFunction 2 3 should not make a recursive call to myFunction 2 3
It would be really useful if a debugger/interpreter could detect when
this type of error happens and generates an error message documenting
the location of such an infinite loop call.
A more sophisticated version would detect more complex repeat patterns and
output those.
A lesser version would be some way to assert that a recursive function
call really does reduce based on the definition of
reduce for the particular function, but that imposes more work on the
programmer. (Eiffel does this)
> Finding infinite loops in functional programs is quite hard. Colin
> Runciman and Jan Sparud have been working on "redex trails". We
> plan to help at least identify where the loop is by putting out
> cost-centre-stack information... but that's still in the works.
Of course it would be much nicer if the compiler rejected all
functions for which it could not prove that there was no way for
the function to enter an infinite loop, but I don't know enough theory to
know whether that is possible. I take your paragraph to mean that it
is not impossible but it is hard.
So to bring this back to my original question, I am trying to figure out
how to think about debuging Haskell code. At least for me, the
application of assertions to Haskell programming is non-intuitive.
If you could explain how you expect people to use assertions in day-to-day
functional programming/scripting to write better code, that would be
really helpful.
-Alex-
___________________________________________________________________
S. Alexander Jacobson i2x Media
1-212-697-0184 voice 1-212-697-1427 fax
