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