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

[address@hidden]

Dan Weinreb <dlw@exceloncorp.com> writes:

>    Date: Thu, 10 Jan 2002 12:59:09 -0500 (EST)
>    From: Guy Steele - Sun Microsystems Labs <gls@labean.East.Sun.COM>
> 
>    Careful, here, Dan; taking this to a logical extreme
>    implies that, if you beef up the contracts, you can
>    define away all errors.
> 
> I really don't understand what you mean by this.
> 
> Perhaps you're saying that you could define away all errors by simply
> making the contract be the same as the code.  

That's one way, but I think Guy was referring to another.

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'.  Well, you now have a `division' operator that is
`well-defined' on both numbers and strings.  Add some more types to
that clause and suddenly your `division' operator simply cannot fail a
`static type check' because the input to it can be `anything'.

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!

> 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.

> I don't see how to firm up the "in some contexts" in any way better
> than the concept of having contracts, or specifications, at various
> layers of abstraction.  For example, if you define a boolean function
> "prime" whose contract is that it takes a positive integer argument
> and returns a boolean that's true if the argument is prime, and
> someone writes an implementation in which prime(12345) throws
> zero-divide, then that is an error entirely by virtue of the fact that
> the specification for "prime" says that that's not what "prime" is
> defined to do.
> 
> The "in some contexts" seems to mean "it depends on the caller", but
> specifically it depends on the fact that the caller's contract didn't
> specify that throwing zero-divide was part of the defined behavior.

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.