[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
# Re: transitivity does not imply type-checking

`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.`