Docs: Unclear impersonator-of? situation

[rocketnia]

What version of Racket are you using?

Racket v8.12 [cs]

What program did you run?

At the command-line REPL:

Welcome to Racket v8.12 [cs].
> (define v1* add1)
> (define v1 (impersonate-procedure v1* (lambda (x) x)))
> (define v2 v1)
> (impersonator-of? v1 v2)
#t
> (impersonator-of? v1* v2)
#f

This more or less contradicts the first bullet point in docs for impersonator-of? as of 8.12:

Any two values that are eq? to one another are also impersonator-of?. For values that include no impersonators, v1 and v2 are considered impersonators of each other if they are equal?.

If at least one of v1 or v2 is an impersonator:

• If v1 impersonates v1* then (impersonator-of? v1 v2) is #t if and only if (impersonator-of? v1* v2) is #t.

• [...]

What should have happened?

I think the docs are unclear here. This is a situation where v1 impersonates v1* but (impersonator-of? v1 v2) is not the same as (impersonator-of? v1* v2).

I wouldn't go so far as to say the docs are wrong. This is a situation where v1 and v2 are eq?, so it's technically already described by the sentence "Any two values that are eq? to one another are also impersonator-of?."

I found this confusing because I was approaching the docs to determine "What non-eq? chaperones are considered the "same" for chaperone-of? purposes?" (and the chaperone-of? docs forwarded me here to the impersonator-of? docs). The bulleted list doesn't include any case where both v1 and v2 are impersonators that might be the "same," and it wasn't obvious that the eq? sentence was what I was looking for. The eq? sentence was was grouped with the equal? sentence, and the equal? part was a high-level overview that was redundant with a more detailed description a little later on, so the eq? part was easy to ignore and forget about.

I think rearranging a couple of sentences and inserting an "otherwise" could help indicate that the eq? case is a non-redundant detail and that it actually takes precedence in the case where I had thought I found an inaccuracy:

For values that include no impersonators, v1 and v2 are considered impersonators of each other if they are equal?.

Any two values that are eq? to one another are also impersonator-of?. Otherwise, if at least one of v1 or v2 is an impersonator:

• If v1 impersonates v1* then (impersonator-of? v1 v2) is #t if and only if (impersonator-of? v1* v2) is #t.

• [...]

I laid out my frame of mind as I was consulting the docs here in case anyone has a better idea of how to approach this or wants me to try something more adventurous myself.

If it'd be preferred to leave the docs alone, I'll understand. I did eventually come around to the answer I was looking for on my own, so I don't necessarily count as an existence proof that they're confusing, heh.

[sorawee]

I think your fix makes sense.

The situation is similar to an inductive proof where a correct proof needs, say, P(0) and P(5) for base cases, and P(i) -> P(i+1) for the inductive case. If somehow we forget to mark P(5) as a base case, and try to prove it using the inductive clause, the proof might not go through, because P(4) -> P(5) actually doesn't hold.

In this situation, the first bullet point is an inductive case, and (impersonator-of? v1 v2) should really be a base case. But if we don't read it as a base case, but rather an inductive case, then things go wrong.

[rocketnia]

Hmm, another issue occurs to me. These two bullet points seem to apply in the same cases sometimes:

• If v1 impersonates v1* then (impersonator-of? v1 v2) is #t if and only if (impersonator-of? v1* v2) is #t.

• If v2 is a non-interposing impersonator that impersonates v2*, i.e., all of its interposition procedures are #f, then (impersonator-of? v1 v2) is #t if and only if (impersonator-of? v1 v2*) is #t.

Suppose we have a, an interposing impersonator b of a, and a non-interposing impersonator c of b. Now the question I'm wondering is, what should the result be for (impersonator-of? b c)? The second bullet point suggests the answer is the same as that for (impersonator-of? b b), which is clearly supposed to be #t since b and b are eq?. But the first bullet point suggests the answer is the same as that for (impersonator-of? a c) (and hence (impersonator-of? a b) if we apply the second bullet point next), which is clearly supposed to be #f since there's an interposing impersonator in c and b that isn't preserved in a.

In practice, it seems the second bullet point takes precedence:

> (define a add1)
> (define b (impersonate-procedure a (lambda (x) x)))
> (define c (impersonate-procedure b #f impersonator-prop:contracted #f))
> (eq? b c)
#f
> (impersonator-of? b c)
#t

I think this additional issue can be addressed by swapping the order of these bullet points and adding "Otherwise," or "If v1 is not an impersonator and ..." in between them.

[rfindler]

I wonder if it would help to write down an accurate but optimization-free implementation of chaperone-of? that used a hypothetical "remove one layer of chaperones" function and put that into the docs? (It could even be tested using unsafe operations, I expect.)

Then, the idea would be to get rid of the detailed prose description but just keep a high-level prose description.