Type Systems as Macros

Awesome! Would love to check it out once you have a prototype.

This is a little more general. They implement a stack of type systems all the way up to F-omega, and they're able reuse and compose the macro libraries to make the more elaborate type checkers. It's pretty impressive.

Typed Racket runs after macro expansion, performing analysis on fully-expanded code. This technique runs as part of macro expansion, rather than after. The upshot is that macros get to use and generate type information, so language and type system features like typeclasses or GADTs can be library-provided macros.

Typed Racket uses macro expansion to translate its typed surface language into a typed core language, and then typechecks the core language.

Our approach uses macro expansion to typecheck the surface language and translates it into an untyped core language.

The two approaches should be considered alternative tools in a programmer's toolbox.

It could, though it's not clear whether it would be an improvement.

Typed Racket uses macro expansion to translate its typed surface language into a typed core language, and then type checks that core language.

This approach works well because the surface and core languages are similar, and thus the type checker need only handle a small number of core forms.

This approach is limited, however, to constructs that are translatable into the core typed language. For example, a few Racket `for/X` comprehension forms are not supported in Typed Racket because they are difficult to translate.

Our approach alternatively uses macro expansion to type check the surface language and translates it into an untyped core language. Thus it's less limited in the typed languages one may implement. The tradeoff is that the programmer must implement type rules for all forms in the surface language, rather than just the core language.

> Can you do dependent types?

Yes. For example, see https://github.com/wilbowma/cur

Macros are run at compile time, and are used to rewrite source code prior to interpretation or compilation. They're mostly used to make nicer syntax, e.g. a macro could turn an expression like `(with-file (f "/tmp/foo") ...)` into a working implementation like:

    (let* ((f (open "/tmp/foo"))
           (result ...))
      (close f)
      result)

Here, the authors make macros for type annotations, i.e. they take expressions like `(my-value : my-type)`, check whether the types unify correctly, and spit out an untyped expression implementing that value if they do.

By using macros, the type system becomes modular: new type system features (subtyping, kinds, etc.) can be written by the programmer as a set of macros, rather than as a whole new language (and all of the work that entails). They test their claim by implementing a bunch of features, combining/reusing them in a bunch of mini languages, and write some semi-plausible programs in these languages, to see if they're realistic.