[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*To*: scheme@mit-mc.ARPA*Subject*: assertions are better than types*From*: Will Clinger <willc%indiana.csnet@csnet-relay.arpa>*Date*: Sun, 17 Mar 85 17:21:05 est

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

- Prev by Date:
**I/O proposal** - Next by Date:
**assertions are better than types** - Prev by thread:
**I/O proposal** - Next by thread:
**assertions are better than types** - Index(es):