[racket] Defining a typed language

On Mon, Oct 27, 2014 at 09:43:26AM +0100, Konrad Hinsen wrote:
> It looks like it does the equivalent of adding (require
> a-typed-lang/more) at the beginning of each module that uses
> a-typed-lang. That's what I expected my original code to do as
> well.

Yep...  Your version was very nearly correct, and I wouldn't have been able
to find a working solution if I hadn't seen that first.  The missing piece
is basically dealing with macro hygiene:

  http://docs.racket-lang.org/guide/pattern-macros.html#(part._.Lexical_.Scope)

I seem to recall that the Guide used to have a simple example of inserting
datum->syntax to bypass.  That would be the closest fit to our situation
here, but I can't seem to find it now.  IIRC, it went something
like this:

  (define-syntax-rule (define-foo)
    (define foo 3))

  (define-foo)
  (displayln foo)
    ; ...doesn't work.  compile time error:  "identifier not bound."
    ;   tell-tale sign of needing datum->syntax!  (or, preferably,
    ;   passing the identifier as an argument, syntax-parameterize, etc.).

The fix being...

  (define-syntax (define-foo ix)
    (syntax-case ix ()
     [(_)
      (with-syntax ([fix (datum->syntax ix 'foo)])
        #'(define fix 3))]))

  (define-foo)
  (displayln foo)
    ; ...does work.

Personally, I tend to think of macro hygiene as being like conservation
of energy---sort of a "conservation of identifiers."  A macro can't
output an identifier that it didn't take in as input.  (Unless we
explicitly override, like we're doing above.)

I have to admit that I never really understood this until I sat down
at a running system and tried to recreate define-foo from memory.
And then various iterations, extensions, stress-tests, etc.
For example,

  (define-syntax-rule (define-foo-neo) (define-foo))

This can't work, since define-foo-neo takes zero identifiers
as input and attempts to produce one as output, which would violate
"conservation of identifiers."  (I guess I should probably emphasize
that the real/official terminology is different---and more refined.
See Matthew Flatt's recent post for a nice example.)

[Aside...   This was actually the reason I download Racket in the first
place:  I wanted to learn how to do macros the Scheme way before
learning them the Scala way.  (I kind of wish that the charms of the
module system were equally well known.)]

Eli Barzilay's paper also helped a lot:

  http://barzilay.org/misc/stxparam.pdf

Among other things, this has an accessible explanation of some of
the downsides of datum->syntax.

> A final question: after a quick look at the documentation for impersonators,
> this looks like a check that foo is indeed the original function foo and
> not something wrapped in a contract, right?

Right...  In your original message, you mentioned wanting to avoid the
overhead of redundant redundant contracts, which is a topic that I'm
keen on, as well.  [In my scenario, it'd be more like importing extracts
from a (much) stronger, external type theory---but same basic problem.]

Thanks...  Evan