[racket] Typed Racket macros in untyped code

On Thu, Sep 15, 2011 at 10:29 PM, Eric Dobson <eric.n.dobson at gmail.com> wrote:
> Currently macros written from Typed Racket can not be used in the
> untyped world.
> Example:
>
> #lang racket/load
>
> (module t typed/racket
>  (provide foo)
>  (define-syntax (foo stx)
>    #'(+ 2 1)))
>
> (module u racket
>  (require 't)
>  (displayln (foo)))
>
> (require 'u)
>
> This was brought up on the list a while ago, and the answer was that
> when the certificate system needed work before this was feasible. My
> question is: are taints the feature that was needed? And has any
> progress been made towards this?

Yes, taints are the right thing here.  I was just thinking this week
about what the right strategy is here, and it shouldn't be too hard to
implement.

To explain a little more about what the problem was, and why taints
fix it, consider the following modules:

#lang racket/load
(module m1 typed/racket
   (: f : Number -> Number)
  (define (f x) (add1 x))
  (define-syntax-rule (g e) (f e))
  (provide g))

(module n racket
  (require 'm1)
  (define-syntax (cheat stx)
    (syntax-case (local-expand #'(g 0) 'expression null) ()
       [(app f _)  #'f])
  ((cheat) 'bad)))

This is obviously not ok, since we're passing 'bad to `f'.  The
solution is to rewrite `m1' to this:

(module m1 typed/racket
   (: f : Number -> Number)
  (define (f* x) (add1 x))
  (define/contract contract-f (number? . -> . number?) (lambda (x) (add1 x)))
  (define-syntax (f stx) (if typed-context? (taint #'f*) (taint #'contract-f)))
  (define-syntax-rule (g e) (f e))
  (provide g))

Now our bad module can't get the bad identifier, because `g' doesn't
have a reference to it, and the taints ensure that even a conspiracy
between a typed and and untyped module can't expose the internal
version of `f'.

> Also as a work around the following program works:
>
>
> #lang racket/load
>
>
> (module t2 racket
>  (require typed/racket)
>  (provide foo)
>  (define-syntax (foo stx)
>    #'(let ()
>        (: x Number)
>        (define x (sqrt 2))
>        x)))
>
>
> (module u2 racket
>  (require 't2)
>  (displayln (foo)))
>
> (module tu2 typed/racket
>  (require 't2)
>  (: y Number)
>  (define y (foo))
>  (displayln y))
>
> (require 'u2)
> (require 'tu2)
>
> Which seems to achieve what TR is currently preventing. Is this
> unsafe/buggy, or is there another reason why it works when the
> language is not typed?

This works because the `foo' macro hasn't made any promises about
being typed, and can't refer to any typed identifier without going
through a contract.  It's just like a regular untyped macro, except
that it includes uses of the `:' form.  The only way to get Typed
Racket to let you call yourself typed, or use any typed values without
a contract, is to be checked by the typed version of `#%module-begin',
which `foo' is not.  So there's no danger here.
-- 
sam th
samth at ccs.neu.edu