[racket-dev] A tricky chaperone puzzle

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" <robby at 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
> <robby at 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 <mflatt at 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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.racket-lang.org/dev/archive/attachments/20140724/555d43df/attachment.html>