Re: cheerful static typing (was: Any and Every... (was: Eval))

[Dan Weinreb <address@hidden>]

   Date: 10 Jan 2002 14:30:15 -0500
   From: jmarshall@mak.com

   Considering the problem of division (and division by zero), you may
   think it is reasonable to consider `an exception is thrown if the
   divisor is zero' to not be an error but rather part of the `contract'
   of divide.  But what about `an exception is thrown if the divisor is a
   string'.  

I'm not sure what you mean by "what about".  That doesn't happen in Java,
because the problem is always caught "statically" rather than causing an
exception at runtime.  It's a contract violation and it's an error.

   But this isn't at all what *I* have in mind when I write software.  If
   I were to write (/ 42 x), where X is bound to a string, my intent
   probably was *not* to `correctly' invoke the error handler, but rather
   not to have written the expression in the first place!

Well, come on now.  Suppose I'm trying to compute the mean of two
numbers and I write, using Lisp syntax since you are, (/ (+ x y) 3).
That's an error because my implementation doesn't match my contract.
As I said before, an error doesn't necessarily throw an exception, and
it doesn't necessarily get flagged automatically at compile time.

   > To put it another way, I don't see what "correct" can mean other than
   > that the code does, in fact, provide an implementation of a
   > specification of what the code is supposed to do.  

   It can mean that the code matches the intent of the programmer.  While
   it is true that this is hard to define rigorously, it *is* worthwhile
   to consider.

When I talk about "specification" or "contract", I mean the intent
of the programmer.

   Ok, but what should   prime ("hello there")  do?  Throwing an
   exception isn't in the contract (well, the caller is supposed to honor
   the `positive integer' part, but we all make mistakes).  If you extend
   the contract with a default clause of `otherwise, throw an exception',
   then certain kinds of contract violations can no longer exist by
   definition.

In light of this, now I understand what you mean and what Guy meant.
Right, it's pretty pointless to write a contract in which a throw of
any kind of exception at all is considered to be part of the contract.
What I would consider a typical contract would in general specify
certain exceptions that are supposed to be thrown in response to
certain input parameter values or state observed from elsewhere, and
then if any *other* exceptions than those are thrown, then such
exceptions are considered to denote an error.

A few months ago I looked all over for published literature on this
kind of thing.  The paper "Exception Handling" by Flaviu Cristian is
the best thing I've found on this topic, and expresses what I'm trying
to say in a much more specific and clear way.  It's "as formal as
necessary, but no more formal".