Re: Bindings and guard-based auditing

On May 25, 2010, at 11:03, Thomas Leonard wrote:

> For the slots-only case, I'm imagining that there's some method on  
> Slot
> to get details for an auditor (getAuditionInfo or some-such). This is
> only called for known slot types (FinalSlot, VarSlot, etc). For other
> slot types, we pass no information to auditors.
>
> (yes, this makes some slot types special, but as I understand it the
> bindings proposal makes certain binding types special)

What do you mean by "binding types"?

Bindings are not typed: they consist of the pair (slot, guard the slot  
passed) and happen to be stored as CoercedSlot objects ('slot' here  
means 'collection of one value'; the CoercedSlot is *not*  
participating as a slot in the environment).

Note that 'CoercedSlot' does not mean 'a (container for a) slot which  
has been coerced'; it means 'a slot whose value *has been* coerced';  
it is basically GuardedSlot without the mutability.

> These cases would be the same (assuming the built-in slot types used  
> in
> the expansion give up their guard to auditors):
>
>  def x := 3
>  def x :int := 3
>  var x := 3
>  var x :int := 3
>
> But in:
>
>  def &x := makeSlot(...)
>
> the information given up to an auditor would depend on makeSlot  
> (whereas
> with bindings no information is given up), and in

Is 'makeSlot' here a builtin or some user-defined function?

> For wacky slots:
>
>  def &&wacky := makeCoercedSlot(WackySlot, makeWackySlot(value))
>
> becomes
>
>  def &wacky :CoercedSlot[WackySlot] := makeWackySlot(value)
>
> where CoercedSlot is a trusted slot type which simply proxies to the
> underlying slot, coerced by the guard. It gives up the guard  
> (WackySlot)
> to the auditor, which can process it as it pleases. makeWackySlot  
> could
> do the coercion itself if desired.

I don't see what this CoercedSlot (please don't call it that, BTW;  
this is different from what CS in the GBA proposal does) adds;  
wouldn't it be sufficient to have the following?

    def &wacky :WackySlot := makeWackySlot(value)

In current (pre- or post-GBA) E semantics, this coerces the rvalue by  
WackySlot before storing it as the slot for 'wacky'.

...Oh, I see. We put the slot in a wrapper which is known to give  
reliable information to the auditors; in this particular case 'the  
behavior of this slot, as a slot, is that enforced by WackySlot'.

> The main difference is that bindings add new syntax (&&x and "def ...
> as").

As a historical note:

The && syntax was added primarily so that sugar expansions which  
rebind values (such as &&, ||, and 'extends') can preserve binding  
guards.

The 'as' syntax was added so that the bindings of object definitions  
could have information for auditors, without having to write e.g. def  
foo :DeepFrozen := {def foo implements DeepFrozen { ... }}.

How does your proposal handle the latter case? That is, in

   def foo implements ... {
     ...
   }

   def bar implements Nonsklarkish {
     ... foo ...
   }

how does the programmer control the amount of information about foo  
which can be observed by Nonsklarkish when auditing bar?

-- 
Kevin Reid                                  <http://switchb.org/kpreid/>