Re: transitivity does not imply type-checking

[Jens Axel Søgaard <jensaxel@xxxxxxxxxxxx>]

Matthias Radestock wrote:
> In section "Why are <? etc. procedures, not macros?" of the srfi
> document it says
>
> <quote>
> ... 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.
> </quote>
>
> 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)

and

   (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