What is the general class of programs that have this difficulty? (Does it include the example from Matthew's "you want it when?" paper about structs?)
I'm not getting why typed racket has to do something special here to deal with this box. That is, by the time typed/racket gets a hold of the expanded program things seems pretty simple. That is, where do the savings come from by disallowing this program? Robby On Mon, Jun 21, 2010 at 2:15 PM, Sam Tobin-Hochstadt <[email protected]> wrote: > The following program implicitly does something like `provide', via mutation. > > #lang racket/load > > (module store racket > (define s (box #f)) > (provide s)) > > (module m typed/racket > (require (for-syntax 'store)) > (define: (x) : Number 1) > (begin-for-syntax (set-box! s #'x))) > > (module n typed/racket > (require (for-syntax 'store) 'm) > (define-syntax (mac stx) > (define myx (unbox s)) > #`(add1 (#,myx))) > (mac)) > > (require 'n) > > The certificate system currently allows this, although it's not > obvious to me that it should. Typed Scheme also ensures that it > typechecks. However, Typed Scheme could save a bunch of work at > startup if this didn't have to typecheck. What do people think is the > right tradeoff? Does anyone care about programs like this? Should > the certificate system allow them? Should Typed Scheme make them > work, at the cost of some performance? > -- > sam th > [email protected] > _________________________________________________ > For list-related administrative tasks: > http://lists.racket-lang.org/listinfo/dev > _________________________________________________ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/dev

