[racket] Defining a typed language

On Mon, Oct 27, 2014 at 05:43:38AM -0400, Alexander D. Knauth wrote:
> So it didn’t work if (require a-typed-lang/more) was in
> a-typed-lang/main.rkt, it didn’t work, but commenting that out made it
> work again.
> 
> Does anyone know what’s happening here?

That'd happen in my version, too, if a (require a-typed-lang/more) was left
in main.rkt.  Typed Racket does some black magic with global, mutable state
at the for-syntax level---as Sam T-H mentioned last month---which means
that things don't always compose as well as you'd expect.

Here's a simple example that exhibits even more surprising behavior:

  -- a-typed-lang/main.rkt -------------

  #lang typed-racket/minimal

  (require typed/racket
           "andromeda-strain.rkt")

  (provide (all-from-out typed/racket))

  -- a-typed-lang/andromeda-strain.rkt -

  #lang typed/racket

  (require "scoop.rkt")

  ; *no* provide.

  -- a-typed-lang/scoop.rkt ------------

  #lang typed/racket

  (require "more.rkt")

  ; none here, either.

  -- a-typed-lang/more.rkt -------------

  #lang typed/racket

  (provide foo)

  (: foo (Integer -> Integer))
  (define (foo x)
    (* 2 x))

  -- example.rkt -----------------------

  #lang a-typed-lang

  (require a-typed-lang/more)

  (displayln (foo 5))
    ; ...doesn't work.  compile-time error:
    ;   "untyped identifier blame1 imported", etc.

Note how the extraneous require can infect example.rkt, even across
several layers of indirection.  (And most of them don't
request any identifiers in the first place.)  That's the global
state at work.

The particular bit of mutable infrastructure that's causing trouble
above can be seen by decompiling more.rkt, rendered here with some
simplifications and human-readability tweaks:

  (define-syntax foo
    (if (unbox typed-context?)
        (make-rename-transformer #'original-foo)
        (make-rename-transformer #'wrapped-in-a-contract-foo)))

This is what allows TR to automatically expose chaperoned
functions to untyped importers, while allowing unsupervised access to
typed ones.

Unfortunately, in the #lang setting, we're requiring more.rkt *twice*,
and the first import sees the wrong context (#&#f).  This means that
foo is stuck as the wrapper-producing transformer, forever and ever.
Since the typed module isn't set up with bindings for the contract
antibodies that then get emitted (blame1, etc.), an error
occurs at compile time.

[The reason this doesn't cause breakage more frequently is
that modules usually get a separate copy of that mutable
state, due to the phase 1 (re-)instantiation rules.]

Anyway, hopes this helps...  Evan