transitivity does not imply type-checking Matthias Radestock (19 Nov 2005 11:16 UTC)
Re: transitivity does not imply type-checking Jens Axel Søgaard (19 Nov 2005 18:08 UTC)
Re: transitivity does not imply type-checking Matthias Radestock (20 Nov 2005 09:37 UTC)
Re: transitivity does not imply type-checking Jens Axel Søgaard (20 Nov 2005 10:04 UTC)
Re: transitivity does not imply type-checking Matthias Radestock (20 Nov 2005 12:53 UTC)
Re: transitivity does not imply type-checking Jens Axel Søgaard (20 Nov 2005 13:32 UTC)
Re: transitivity does not imply type-checking Matthias Radestock (20 Nov 2005 18:39 UTC)

Re: transitivity does not imply type-checking Jens Axel Søgaard 20 Nov 2005 10:04 UTC

Matthias Radestock wrote:
> Jens Axel Søgaard <xxxxxx@soegaard.net> 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)

You are right of course.

It is

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

and

    (= 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
> situation.

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