[racket] Defining a typed language

On Thu, Oct 16, 2014 at 11:41 AM, Konrad Hinsen
<konrad.hinsen at fastmail.net> wrote:
> Konrad Hinsen writes:
>
>  > After a closer look at the language definition mechanism, I came to the
>  > conclusion that the language here is actually "s-exp", with my module
>  > merely providing the initial bindings.
>  >
>  > So what I seem to need is typed/s-exp, but that doesn't exist. How
>  > would I go about writing this myself? The implementation of s-exp
>  > is simple enough, but I don't see anything in there that says if it's
>  > a typed or an untyped language.
>
> I changed my approach to defining a "full" language, not just a
> variant of s-exp. After exploring how Typed Racket itself is set up, I
> defined a language "test-lang" consisting of the following parts:
>
> -- test-lang/main.rkt ----------------------------
> #lang typed-racket/minimal
>
> (require typed/racket
>          test-lang/more)
>
> (provide (all-from-out typed/racket)
>          (all-from-out test-lang/more))
> --------------------------------------------------
>
> -- test-lang/more.rkt ----------------------------
> #lang typed/racket
>
> (provide bar)
>
> (: bar (-> Integer Integer))
> (define (bar x)
>   (* 2 x))
> --------------------------------------------------
>
> -- test-lang/lang/reader.rkt ---------------------
> #lang s-exp syntax/module-reader
>
> test-lang/main
>
> #:read r:read
> #:read-syntax r:read-syntax
>
> (require (prefix-in r: typed-racket/typed-reader))
> --------------------------------------------------
>
> With those files in place (in a collection), I try to run
>
> -- test.rkt --------------------------------------
> #lang test-lang
>
> (: x Integer)
> (define x 42)
> (print x)
>
> (print (bar x))
> --------------------------------------------------
>
> This results in an error message:
>
> ; test-lang/more.rkt:4:9: Type Checker: missing type for identifier;
> ;  consider using `require/typed' to import it
> ;   identifier: bar
> ;   from module: test-lang/more
> ;   in: bar
>
> But 'bar' in test-lang/more has a type annotation, and if I
> do (require test-lang/more) explicitly, everything works fine.
> So where does the type annotation for bar disappear?

What's happening is that the type annotation for `bar` is communicated
to the type checker for "test.rkt" with an expansion-time side effect.
Unfortunately, for reasons that are complex (and that I don't fully
remember at the moment) the language position doesn't cause all the
side effects we need to happen -- only `require` does that.

My suggestion is to have your `test-lang` language use
`#%module-begin` to expand into `(tr:module-begin (require
test-lang/more) user-program-here ...)`, which should fix the problem.

Sam