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

[Zooko <address@hidden>]

Folks:

It sounds to me like exceptions serve two purposes: (a) signal contract 
violation, (b) rare, non-local control flow.

This is consistent with my experience as a working programmer in C++, Java, and 
Python: sometimes exceptions are used to mean that there is a serious error in 
the source code, and other times they are used to simplify control flow among 
nested function calls.


Hm.  Okay, now I begin to see GLS's point.  You could see the contract that the 
division operator offers as requiring the caller to provide a non-zero divisor, 
and raising an exception is a way to signal contract violation, or you could see 
the contract as requiring any integer divisor from the caller, and simply 
offering different behavior if it is zero.

Very interesting.

Perhaps this is part of why exceptions are more useful than simple program 
termination -- that they allow the caller to dynamically "extend" the contract
that the callee offers by handling exceptions from the original contract.

Now I can think of a case where almost everyone would agree that the caller 
should not do that.  Suppose there is a precondition which cannot be 
efficiently programmatically tested, but is documented and *partially* tested:

;; @precondition: `arg' must be prime
(define (thingiemabob arg) ((if (equal arg 4) (raise "precondition violation")) ... ))

Now I'm sure we all agree that invoking this method with an argument that might 
be prime or 4 or 6 and catching the exception, is flatly wrong.  What about 
invoking it with an argument that might be prime or 4 and catching the 
exception?  It still feels wrong to me.


Okay, this is what I think I will do in the future:

1.  When writing a callee, think of the contract that it offers as a nested set 
of contracts.  "You can call my division operator with a non-zero integer 
divisor, and I'll return the result.  *or* We can extend this contract so that 
you can call with any integer divisor and I'll raise an exception if it is zero, 
else return the result."

2.  Think of dynamic type-checks as added layers of nested contract that the 
programming language wraps around every callee's contract.  "Since this division 
operator is written in the Zweep language, you automatically have this added 
optional clause in the contract:  '*or* You can call with an incorrect type and 
I'll raise an exception if it isn't the right type, else I'll fulfill one of the 
previous clauses in this contract.'"

3.  When writing the *caller*, you really ought to tend towards relying on the 
inner layers of the contract.  ;-)  The outer layers are less well understood by 
other programmers and less frequently used, and they are also more general which 
reduces the ability of your tools to help you detect errors in their use.  In 
this particular example, it is nicest to ensure that you have a non-zero divisor 
for starters (or to propagate that requirement up to *your* caller).  
Occasionally you may prefer to have any integer divisor and to catch the 
exception.  Very rarely, you may need to call with any typed divisor and catch 
the exception if it isn't an integer.  (When?  It's all about simplifying 
control flow I think.)

4.  There are some limits to how general the contract can become.

4.a.  One of these is if you can't automatically detect a violation of layer N, 
then you cannot use such detection to define layer N+1.

4.b.  Another is an agreement among programmers: "Nobody on this team will ever 
deliberately invoke `divide' with a divisor that might not be an integer and 
then catch the ArithmeticException!  It's not that doing so is inherently wrong, 
it's just that agreeing on this rule allows us to make simplifying assumptions 
when reading each other's code, and to put our type-checking tools to better 
use.".

4.c.  Then there is bilateral agreement between implementors of the caller and 
the callee.  If the person who implemented the `divisor' operator left a note 
saying "@precondition: divisor must be non-zero", then it is bad form for you to 
extend his contract willy-nilly.  It would be better for you to change his 
contract, removing the "@precondition" and adding "@raises ArithmeticException 
if divisor is zero".


I guess this doesn't really crystallize the distinction that we are discussing, 
but I think it does add some detail, and furthermore it is what I intend to do 
in practice in the future.  Note that parts 1, 2, and 4.a. are "hard" and 
parts 3, 4.b., and 4.c. are "soft and fuzzy".  Nonetheless those soft parts seem 
to be important engineering practices.


Regards,

Zooko

---
                 zooko.com
Security and Distributed Systems Engineering
---