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 <div class="gmail_quote">On Jul 24, 2014 7:54 PM, "Robby Findler" <<a href="mailto:robby@eecs.northwestern.edu">robby@eecs.northwestern.edu</a>> wrote: <blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"> Ah, nope. That model doesn't include function chaperones! Robby On Thu, Jul 24, 2014 at 6:14 PM, Robby Findler <<a href="mailto:robby@eecs.northwestern.edu">robby@eecs.northwestern.edu</a>> 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 <<a href="mailto:mflatt@cs.utah.edu">mflatt@cs.utah.edu</a>> 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: >>> <a href="http://lists.racket-lang.org/dev" target="_blank">http://lists.racket-lang.org/dev</a> >> >> _________________________ >> Racket Developers list: >> <a href="http://lists.racket-lang.org/dev" target="_blank">http://lists.racket-lang.org/dev</a> </blockquote></div>