What's the common idea to represent types in Racket's LOP?

Questions & Answers
1

Hi all,

I'm new to designing languages in Racket and need some help with general techniques.

Suppose I want to build a statically typed language (s-exp) on top of Racket.

In my opinion, For the surface language, what macros would do is

  1. parse the code, store types into some context and return the valid Racket code (modelled as untyped λ-calculus) after type erasure and/or coercion (if with subtyping).
  2. before return the whole program, the types should be analysed and type checked in some meta-function like subtyping and typing.

Then my question is, how to represent types in the compilation phase, and how to define such function to compute the types.

In a setting of writing an interpreter in Racket (without macros), the types can be a symbol or a struct, the subtyping is Type -> Type -> Bool and the typing is Context -> Term -> Type.

I've checked the source code of turnstile since it also targets to type checking. But it seems involved with ideas and tricks I'm not familiar with because I just know some basic notions of macros.

2

Consider another phase is still the usual racket, everything still can be used with require (for-syntax ...), so I would say it's very flexible. What I usually use is rewrapping on existing structure

(define-syntax-parser #%datum
  [(_ . n:number) (syntax-property #'n 'type 'Number)]
  ; etc ...
  )
(define-syntax (define stx)
  (syntax-parse stx
    [(_ name:id ty:type exp:expr)
     (define exp-ty (syntax-property (local-expand 'expression #'exp '()) 'type))
     (unify (normalize #'ty) exp-ty)
     #'(define name exp)]))

Although this can go far, it's like dancing on the edge of a cliff.

The simplest way I know is to define #%module-begin and #%top-interaction

(define-syntax-rule (top-interaction e)
  (begin
    (printf "type:- ~a~n" (pretty-print-typ (type/infer (parse e))))
    (parse e)))

(define-syntax-rule (module-begin e* ...)
  (#%module-begin
   (top-interaction e*) ...))

The big parse is to build your AST

(define-syntax (parse stx)
  (define-syntax-class bind
    (pattern (bind-name:id bind-expr)
             #:with bind
             #'(cons (symbol->string 'bind-name) (parse bind-expr))))
  (syntax-parse stx
    #:literals (let λ)
    ; (let ([a 1]
    ;       [b (λ (x) x)])
    ;   (b a))
    (`[let (binding*:bind ...) body]
     #'(expr:let (list binding*.bind ...) (parse body)))
    (`[λ (ps* ...) body] #'(expr:lambda (list (symbol->string 'ps*) ...) (parse body)))
    (`[(~literal quote) (elem* ...)] #'(expr:list (list (parse elem*) ...)))
    (`[f arg* ...] #'(expr:application (parse f) (list (parse arg*) ...)))
    (`v:id #'(expr:variable (symbol->string 'v)))
    (`s:string #'(expr:string (#%datum . s)))
    (`b:boolean #'(expr:bool (#%datum . b)))
    (`i:exact-integer #'(expr:int (#%datum . i)))))

Thus, later you only work on normal structure and well-known racket.

You might also need to consider reforming the module: Compilation-time Environment · GitHub

3

There are of course several ways of doing this.

One approach is to represent types as structures.
As an example here is how types are represented in minipascal:

See "compiler.rkt" for how the compiler compiles type declarations.