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

Re: transitivity does not imply type-checking

Jens Axel Søgaard <jensaxel@xxxxxxxxxxxx> writes:

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

That is a very unusual interpretation of transitivity. The ordinary
definition of transitivity is
  (x P y) and (y P z) => (x P z)
We can extend the domain of = etc to all values (NB: R5RS allows that,
but certainly does not require it). For P to still be a predicate it
must return #t/#f, and nothing else. I think you are trying to extend
the range to #t/#f/all-errors, but then P is no longer a predicate and
hence the usual transitivity rule has nothing to say about that

Furthermore, even with the above rule in place it is possible to
construct predicates that do not perform type checking on all args, as I
demonstrated by the example in my previous post.

FWIW, R5RS provides a much more direct hint regarding type checking of
args.(*) In section 1.3.2 it states

"it is an error for a procedure to be passed an argument that the
procedure is not explicitly specified to handle"

Since section 6.2.5 defines the domain of numerical predicates to be
real numbers (and complex numbers for =), it is clear that "it is an
error" to pass any arguments outside that domain.

However, as is usual in R5RS, there is a way around that. First of all,
section 1.3.2 also states that "Implementations may extend a procedure's
domain of definition to include such arguments.", and that "it is an
error" refers to error situations that "implementations are not required
to detect". Hence really anything can happen when you pass an argument
of the wrong type to a predicate.

(*) Thanks to Anton van Straaten for pointing this out.