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

Re: transitivity does not imply type-checking

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

R5RS states that = must me transitive, if one interprets this
to mean that

   (= o1 o2 o3)


   (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)

You are right of course.

It is

   (let ([t1 o1] [t2 o2] [t3 o3])
     (non-short-circuting-and (= t1 t2) (= t2 t3)))


   (= o1 o3)

that should have the same behaviour.

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

I was just saying *if* you make that interpretation, you need to
type check all arguments. If you don't you end up with unspecified
behaviour. In srfi-67 the choice was made to require type-checking of arguments to compare functions in order to avoid unspecified situations.

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.

Yes - those paragraphs are the reason, I wrote the result of = on non-complex arguments is unspecified in R5RS.

Jens Axel Søgaard