Kernel: rationale for not listing bindings

Understanding Kernel's rationale for not listing bindings

As I blogged, I have been reading about Kernel, a better Scheme.

One thing Kernel will not do is to list all of an environment's bindings. At first glance this seemed wrong, because the first rationale that I read for it seemed to contradict itself:

From (§6.7.1)

Presenting [$binds] as a library feature drives home the point that it doesn't introduce any capability that wasn't already provided by the language. In particular, for purposes of type encapsulation (§3.4), there is still no way for a Kernel program to generate a complete list of the variables exhibited in an arbitrary environment. Predicate $binds?, or the techniques used to derive it, could be used to formally enumerate such a list, by sequentially generating all possible variables (an infinite sequence) and testing each one; but there would be no way to know when all variables in the environment had been enumerated. This nontermination is critical because it means that no Kernel program can prove in finite time that two non-eq? environments are equivalent up to mutation; therefore, the rules governing predicate equal? (§4.3.1) do not require it to return false in any cases where predicate eq? returns true.

I read it thru 3 times, and he seems to have accidentally flipped polarity in his argument: He wants to avoid a situation where (called on two objects) eq? would give false and equal? true. But the thing that he fears will give rise to it is being able to completely compare non-eq? environments.

When I read this I got the impression that his rationale was mistaken. But then when I read the paper again, I saw a better rationale elsewhere.

Better rationale

When introducing environments, he gives a different rationale for linking equal? and eq? on environments:

(§4.8)

The behavior of equal? is tied to that of eq? to forestall the possibility of an implementation compromising the encapsulation of the type by allowing a program to determine, in finite time, that all bindings for one environment are the same as those for another. (Cf. the rationale discussion for the derivation of library predicate $binds?, §6.7.1.)

And (§4.9) reinforces it:

There is no need for this module to assume the Equivalence under mutation module, because environments are eq? iff they are equal? .

So the discussion in §6.7.1 was misleading. Now it seems that:

• He fears that listing bindings will compromise the encapsulation of the environment type.
• So he wants equal? and eq?, called on two environments, to always give the same answer.

Why does he want the environment type to be encapsulated in this way? Apparently to prevent mutation of parent environments. Also from (§4.8):

First-class environments offer a tremendous amount of control over what can be accessed from where - but only if there are limitations carefully placed on what can be done without explicit permission. In particular, whenever a combiner is called, it has the opportunity, in principle, to mutate the dynamic environment in which it was called. This power is balanced by omitting any general facility for determining the parents of a given environment, and also omitting any other general facility for mutating the parents, or other ancestors, of a given environment. (For an example of articulate environment- access control, see $provide!, §6.8.2.)

But what's the threat?

This unfortunately does not make it clear what the threat is. I just can't see any exploit that could use `list-bindings' to do something bad.

All I can guess is that it's that misbehaving code could get a list of all current bindings and comprehensively rebind all of them and thus fake the original environment, parents and all. But this is not the same thing as mutating that parent environment. And since one can sometimes correctly guess all the bindings, it is not clear how one can expect this to always work.

Why I suspect this prohibition isn't needed

Here's a positive argument that this prohibition is wrong: Containers such as alists can hold the same data that environments do: A set of bindings. Yet there is no problem being able to list all the elements of an alist or to compare alists `equal?' (and Shutt doesn't say there is).