[racket-dev] RFC: "provide" via mutation

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 <samth at 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
> samth at ccs.neu.edu
> _________________________________________________
>  For list-related administrative tasks:
>  http://lists.racket-lang.org/listinfo/dev
>