Re: transitivity does not imply type-checking

[Sebastian Egner <sebastian.egner@xxxxxxxxxxx>]

Matthias wrote:
> 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.

Actually, when SRFI 67 got made we tried to find out
what the
authors of R5RS actually meant by saying (R5RS, Section
6.2.5.):

<quote>These predicates are required to be transitive.


Note: The traditional implementations of these predicates
in
Lisp-like languages are not transitive.</quote>

Unfortunately, it is not clear what the authors of
R5RS mean
by requiring a 'predicate' to be 'transitive.' There
are (at
least) two possible interpretations:

   #1 The order (or equivalence) relation
R represented by <=
(or =) is transitive, in the usual (mathematical)
sense you 
described, i.e. for all x, y, z from the set of possible

argument values:
   (<= x y) => #t   and  
(<= y z) => #t   implies   (<= x z) => #t. 
The set of possible argument values are represented
by 
(REAL? x) => #t for <, <=, >, >=, and
by (NUMBER? x) => #t for ="">
unless the implementation chooses to extend it.

   #2 The predicate procedure tests if the
argument values form
a chain, i.e. (<= 1 2 3) => #t, and (<= 2
1 3) => #f.

As you pointed out, the choice of interpretation has
subtle
implications on semantics---and I do not find either
of them
the clear 'this is what is meant' winner. Let me explain
this in greater detail.

Although #1 seems the obvious choice, it does not
really make a
lot of sense because = is already defined to be equality,
which
by definition is transitive. My doubts got stronger
by the claim
that other Lisp-like languages manage to define non-transitive
'equality.' Miracles and wonders! What does that refer
to? Maybe
(= nan nan) => #f, as IEEE 754 wants it?

Now #2 is not very compelling either because it gives
a rather
unfamiliar meaning to the word 'transitive,' but it
could be
that transitivity was the word that came to mind at
the time.

Anyway, in #2 you have a very nice property: After
evaluating
the test (<= x y z), you have (and (real? x) (real?
y) (real? z))
as a post-condition. In #1, the order of testing is
unspecified,
so (<= x y z) could be implemented as (and (<=
x y) (<= y z)) but
also as (and (<= y z) (<= x y)). In the first
case, (<= 2 1 'a)
does not raise an error, in the second case it does.
In #1 the 
only thing you can say about the arguments after the
test is 
that at least two of them satisfy real?.

For clarification, I was seeking advice from one or
more of the
authors of R5RS to find out what they meant when they
required
<= etc. to be 'transitive.' Unfortunately, neither
me nor our
editor got any clarifying response. (But we also did
not make
it our purpose in life---just a few emails.)

At this point, we cut the theory, ran our favourite
Scheme
systems, typed in (<= 2 1 'a), and looked what
happened: PLT
and Scheme48 both complain about the type mismatch,
i.e. they
type check all arguments whether needed for the result
or not.

So, since we wanted (chain<=? compare-real x1 x2
x3 ...) to be
exactly backward compatible with (<= x1 x2 x3 ...),
we decided
to require the type checking---and of course to be
consistent
this must then be done everywhere. Frankly, I am quite
happy
with this choice because it contributes to robustness,
more
than it hurts performance---unless you use chain<=?
on very
long lists, in which case I would recommend not using
APPLY
on an argument lists but rather another 4-line-program:

(define (vector-chain<=? compare vec)
  (every?-ec (:range i 1 (vector-length vec))
             (<=?
compare (vector-ref vec (- i 1))
               
          (vector-ref vec i))))


;-)

Sebastian.