[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: transitivity does not imply type-checking
> 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
Actually, when SRFI 67 got made we tried to find out
authors of R5RS actually meant by saying (R5RS, Section
<quote>These predicates are required to be transitive.
Note: The traditional implementations of these predicates
Lisp-like languages are not transitive.</quote>
Unfortunately, it is not clear what the authors of
by requiring a 'predicate' to be 'transitive.' There
least) two possible interpretations:
#1 The order (or equivalence) relation
R represented by <=
(or =) is transitive, in the usual (mathematical)
described, i.e. for all x, y, z from the set of possible
(<= x y) => #t and
(<= y z) => #t implies (<= x z) => #t.
The set of possible argument values are represented
(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
implications on semantics---and I do not find either
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,
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
(= nan nan) => #f, as IEEE 754 wants it?
Now #2 is not very compelling either because it gives
unfamiliar meaning to the word 'transitive,' but it
that transitivity was the word that came to mind at
Anyway, in #2 you have a very nice property: After
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
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
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
<= etc. to be 'transitive.' Unfortunately, neither
me nor our
editor got any clarifying response. (But we also did
it our purpose in life---just a few emails.)
At this point, we cut the theory, ran our favourite
systems, typed in (<= 2 1 'a), and looked what
and Scheme48 both complain about the type mismatch,
type check all arguments whether needed for the result
So, since we wanted (chain<=? compare-real x1 x2
x3 ...) to be
exactly backward compatible with (<= x1 x2 x3 ...),
to require the type checking---and of course to be
this must then be done everywhere. Frankly, I am quite
with this choice because it contributes to robustness,
than it hurts performance---unless you use chain<=?
long lists, in which case I would recommend not using
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))))