assertions are better than types

[Will Clinger <willc%indiana.csnet@csnet-relay.arpa>]

Gerry's numbers proposal is the first attempt I've ever seen at 
doing numbers right, and I'm very excited about it.  I've become 
concerned about the effectiveness of the type-restricted 
operators, however, and I'd like to offer an alternative 
proposal.  

First of all, let me state my understanding of Gerry's proposal, 
as I edited it for the Revised Revised Report.  (I know it isn't 
written very well -- my concern was growing as I wrote it.) 

---------------------------------------------------------------- 


(number op)                                             procedure
(complex op)                                            procedure
(real op)                                               procedure
(rational op)                                           procedure
(integer op)                                            procedure

These procedures take a numeric operator op and return a 
procedure that acts like op except that it is restricted to 
operate on numbers of the specified type and to return numbers 
of the specified type.  The idea of these procedures is 
expressed by 

  (define make-type-restrictor
    (lambda (type?)
      (lambda (op)
        (lambda args
          (if (every type? args)
              (let ((ans (apply op args)))
                (if (type? ans)
                    ans
                    (error "Bad result from type-restricted operator")))
              (error "Bad argument to type-restricted operator"))))))

  (define number (make-type-restrictor number?))
  (define complex (make-type-restrictor complex?))
  (define real (make-type-restrictor real?))
  (define rational (make-type-restrictor rational?))
  (define integer (make-type-restrictor integer?))

where EVERY returns true if its first argument, a predicate, is 
true of every element of its second argument, a list.  

Some implementations may provide a mechanism whereby the 
programmer can request that these type restriction procedures be 
interpreted as assertions intended to make the code run faster 
rather than as requests for type checks.  

                ((real sqrt) 5)         -->  2.236067977
                ((real sqrt) -1)        -->  error
                ((integer sqrt) 10)     -->  error

The programmer who wrote the last example probably wanted to 
compute (TRUNCATE ((REAL SQRT) 10)).  

[Gerry's rationale would go here.] 

---------------------------------------------------------------- 


My objections: 

1.  Speaking for myself, I would not want to clutter my code 
with all these type-restricted operators as I write the code, 
because it would make the code less readable.  (I guess 
readability is more important to my debugging processes than are 
type checks.) I would be willing to add type assertions when the 
time came to make the code run fast.  Hence for me at least, the 
type restrictions would be more important as advice to the 
compiler than as debugging aids.  

2.  The type restrictors require that all operands and the 
result be of the same type.  This works reasonably well for 
numeric operators but is going to be awkward when the time comes 
to generalize it to other operators.  How am I going to tell the 
compiler that the first argument to vector-ref is a vector of 
strings? 

3.  Statically typed languages are mistaken in associating types 
with variables, and Gerry is on the right track to associate 
type restrictions with operators, but I think most of us would 
agree that the right thing to do is to associate types with 
values.  That leads to my proposal, which follows: 

---------------------------------------------------------------- 


(assert property? obj)                                  procedure

PROPERTY? must be a total (everywhere defined) unary predicate 
with no side effects.  Returns obj.  It is an error if PROPERTY? 
is not true of obj, but implementations are not required to 
detect the error.  

Rationale: In interpreted code, assertions can be used to check 
types, loop invariants, and other assertions.  In compiled code, 
calls to ASSERT have zero overhead but help the compiler to 
produce better code.  The ASSERT procedure is a moby 
generalization of Common Lisp's special form called THE, and of 
MacLisp's FIXNUM-IDENTITY and FLONUM-IDENTITY.  

---------------------------------------------------------------- 


Examples: 

Here is Gabriel's tak benchmark with type-restricted operators 
as in Gerry's proposal: 

(define (tak x y z) 
  (if (not (<? y x))      ; notice that you can't say (integer <?)
      z
      (tak (tak ((integer -1+) x) y z)
	   (tak ((integer -1+) y) z x)
	   (tak ((integer -1+) z) x y))))

Here it is with assertions: 

(define (tak x y z) 
  (assert integer? x)
  (assert integer? y)
  (assert integer? z)
  (if (not (<? y x))
      z
      (tak (tak (-1+ x) y z)
	   (tak (-1+ y) z x)
	   (tak (-1+ z) x y))))

You could also wrap all the references (or calls) to tak in an 
integer declaration, but it's easy to see that that's 
unnecessary.  

Here is doubly recursive Fibonacci: 

; Gerry's proposal 

(define (fib n) 
  (if (<? n 2)    ; notice again that (integer <?) won't work
      n
      ((integer +) (fib ((integer -) n 1)) (fib ((integer -) n 2)))))

; With assertions 

(define (fib n) 
  (assert integer? n)
  (if (<? n 2)
      n
      (+ (assert integer? (fib (- n 1)))
         (assert integer? (fib (- n 2))))))

; With a good compiler, this would suffice.  

(define (fib n) 
  (assert integer? n)
  (if (<? n 2)
      n
      (+ (fib (- n 1)) (fib (- n 2)))))

Of course, if you really wanted fib to run fast, and you didn't 
intend to use it with arguments greater than 40, and excellent 
compilers were widespread, then you would probably say something 
like 

(define fib 
  (let ((fixnum?
	  (lambda (x)
	    (and (integer? x)
		 (not (negative? x))
		 (<? x 100000000)))))
    (rec fib
      (lambda (n)
        (assert fixnum? n)
        (if (<? n 2)
            n
            (+ (assert fixnum? (fib (- n 1)))
	       (assert fixnum? (fib (- n 2)))))))))