I don't quite get the issues yet, but why should this type check? Doesn't it add1 to a function?
Robby On Mon, Jun 21, 2010 at 2:15 PM, Sam Tobin-Hochstadt <sa...@ccs.neu.edu> 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 > sa...@ccs.neu.edu > _________________________________________________ > For list-related administrative tasks: > http://lists.racket-lang.org/listinfo/dev > _________________________________________________ For list-related administrative tasks: http://lists.racket-lang.org/listinfo/dev
