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

Re: transitivity does not imply type-checking

Matthias Radestock wrote:
In section "Why are <? etc. procedures, not macros?" of the srfi
document it says

... one can even require the compare procedures to check the types of
all arguments, even if the result of the comparison is already
known. This is what Section 6.2.5 of R5RS calls ``transitive`` behavior
of the predicates =, <, etc.

It is true that R5RS requires the predicates to be transitive. However,
I cannot see how that implies that unused arguments must be
type-checked, as is asserted in the above.

Take for example the following definition of =:

(define (= x y . rest)
  (and (number? x) (number? y)
       (prim= x y)
       (or (null? rest) (apply my= y rest))))

I claim that this meets the transitivity requirement of R5RS, assuming
prim= is transitive, yet it only type-checks used args.

Since R5RS defines = as

    procedure:  (= z1 z2 z3 ...)

we see that the result of calling = with non-complex arguments
are unspecified.

R5RS states that = must me transitive, if one interprets this
to mean that

   (= o1 o2 o3)


   (let ([t1 o1] [t2 o2] [t3 o3])
     (non-short-circuting-and (= t1 t2) (= t2 t3)))

should behave the same way on all objects o1, o2 and o3, then
type checking all arguments is needed.

If, on the other hand, one only require transitivity when o1,
o2 and o3 are numbers, then type checking all arguments
isn't neccessary.

Jens Axel Søgaard