Yes, true! Robby
On Thu, Jul 24, 2014 at 8:07 PM, Sam Tobin-Hochstadt <sa...@cs.indiana.edu> wrote: > Struct chaperones are the important part, I think. > > But the theorem would be false under option 1, I think. Adding contracts can > add non-contract errors -- the error you get when a you supply the wrong > accessor for struct-chaperone. > > Sam > > On Jul 24, 2014 7:54 PM, "Robby Findler" <ro...@eecs.northwestern.edu> > wrote: >> >> Ah, nope. That model doesn't include function chaperones! >> >> Robby >> >> On Thu, Jul 24, 2014 at 6:14 PM, Robby Findler >> <ro...@eecs.northwestern.edu> wrote: >> > I also lean towards #2. What does the redex model say? Most of those >> > pieces are in it, I think. >> > >> > Robby >> > >> > On Thu, Jul 24, 2014 at 3:25 PM, Matthew Flatt <mfl...@cs.utah.edu> >> > wrote: >> >> Nice example. Offhand, I think that #2 is right, but I'll have to look >> >> at it more to be sure. >> >> >> >> At Thu, 24 Jul 2014 15:45:18 -0400, Sam Tobin-Hochstadt wrote: >> >>> Consider the following module: >> >>> >> >>> (module m racket >> >>> (struct x [a]) >> >>> (define v1 (x 'secret)) >> >>> (define v2 (x 'public)) >> >>> (provide v1 v2) >> >>> (provide/contract [x-a (-> x? (not/c 'secret))])) >> >>> >> >>> It appears that this ensures that you can't get 'secret. But, it turns >> >>> out that I can write a function outside of `m` that behaves like `x-a` >> >>> without the contract: >> >>> >> >>> (require (prefix-in m: 'm)) >> >>> >> >>> (define (x-a v) >> >>> (define out #f) >> >>> (with-handlers ([void void]) >> >>> (m:x-a (chaperone-struct v m:x-a (λ (s v) (set! out v) v)))) >> >>> out) >> >>> >> >>> Now this works: >> >>> >> >>> (displayln (x-a m:v1)) ;; => 'secret >> >>> >> >>> The problem is that `m:x-a` is treated as a >> >>> `struct-accessor-procedure?`, which is a capability for accessing the >> >>> a field, even though it's a significantly restricted capability. >> >>> >> >>> There are a couple possible solutions I've thought of: >> >>> >> >>> 1. Require a non-chaperoned/impersonated accessor. >> >>> 2. Actually use the chaperoned/impersonatored accessor to get the >> >>> value out instead of the underlying accessor. >> >>> >> >>> 1 is a little less expressive. But note that 2 means that you have to >> >>> only allow chaperoned procedures with `chaperone-struct`, and imposes >> >>> significant complication on the runtime. >> >>> >> >>> I favor 1. >> >>> >> >>> Sam >> >>> >> >>> _________________________ >> >>> Racket Developers list: >> >>> http://lists.racket-lang.org/dev >> >> >> >> _________________________ >> >> Racket Developers list: >> >> http://lists.racket-lang.org/dev > > > _________________________ > Racket Developers list: > http://lists.racket-lang.org/dev > _________________________ Racket Developers list: http://lists.racket-lang.org/dev
