[racket] redex + #lang = awesome

On 10/24/12 2:28 PM, Prabhakar Ragde wrote:
> David Van Horn wrote:
>
>> Then I thought, PCF's binding structure is a lot like Racket's: wouldn't
>> it be nice to get syntax coloring, syntax arrows, renaming, etc.  That
>> was about another 30 lines of code.
>
> Can you say a few words about how you achieved this? Thanks to Matthew's
> article and RacketCon tutorial, I now know how creating languages works,
> but he didn't cover this last bit. I could start poring over the code,
> but I suspect a minute or two of your time will save me a lot more.
> Thanks. --PR

Sure!  First, write a redex model.

If you want to create a language, you need a reader.  Since I'm using an 
S-Expression based syntax, this is trivial; here is my reader:

#lang s-exp syntax/module-reader
pcf/langs/pcf

The pcf/langs/pcf.rkt module provide the #%top-interaction and 
#%module-begin forms that implement the language.

The module-begin form is basically the following rewrite:

(_ e ...)
#'(#%module-begin
     (apply values (append (apply-reduction-relation* R (term e)) ...)))

So the program is expanded into a call to apply-reduction-relation* that 
reduces each term using the reduction relation R.  That gets you a 
redex-based #lang language.

Now, if you want to enforce a static discipline, you just make a call to 
your type judgment *at expansion time*:

(_ e ...)
(for-each (λ (e)
             (unless (typable? (syntax->datum e))
               (raise-syntax-error 'type-error "ill-typed" e)))
           (syntax->list #'(e ...)))
#'(#%module-begin
     (apply values (append (apply-reduction-relation* R (term e)) ...)))

Here I'm using the typable? function from my redex model, which is just 
defined as

(define (typable? M)
   (cons? (judgment-holds (typeof () ,M T) T)))

where `typeof' is just the run of the mill typing relation for this 
language.

The top-interaction is similar:

(_ . e)
(unless (typable? (syntax->datum #'e))
   (raise-syntax-error 'type-error "ill-typed" #'e))
#`(apply values (apply-reduction-relation* #,R (term e))

What's left is getting the syntax coloring, renaming, etc.  The key here 
is turn your S-Expression into some piece of Racket code that has the 
same binding structure as the program at hand.  You won't actually *do* 
anything with this Racket expression; it's just there to tell DrRacket 
about the binding structure.  So you do the following:

(_ e ...)
(for-each (λ (e)
             (unless (typable? (syntax->datum e))
               (raise-syntax-error 'type-error "ill-typed" e)))
           (syntax->list #'(e ...)))
#'(#%module-begin
     (lexical e) ...  ;; <<== expand into Racket with lexical structure
     (apply values (append (apply-reduction-relation* R (term e)) ...)))

Where lexical is something like this (it varies based on the particulars 
of the language you're implementing):

(define-syntax (lexical stx)
   (syntax-case stx ()
     ;; throw away the result w/o evaluating
     [(_ e) #'(void (λ () (lx e)))]))

(define-syntax (lx stx)
   (syntax-case stx (λ • : err ⚖)
      [(_ (λ ([x : _] ...) e))
       #'(λ (x ...) (lx e))]
      [(_ (if0 e0 e1 e2))
       #'(if (lx e0)
             (lx e1)
             (lx e2))]
      [(_ (err _ string)) #'string]
      [(_ (• t)) #''(• t)]
      [(_ (c ⚖ e)) #'(begin (lc c) (lx e))]
      [(_ (e ...))
       #'((lx e) ...)]
      [(_ e) #'e]))

(define-syntax (lc stx)
   (syntax-case stx (->)
     [(_ (c0 ... -> c1))
      #'(begin (lc c0) ... (lc c1))]
     [(_ e) #'(lx e)]))

There's one last trick to get arrows from the language to the special 
forms.  That involves syntax-local-introduce, which I think puts that 
feature beyond what should be in such a cute little demo.

But that's the basic idea.

David