I'm glad this has shown up here, I discovered it very shortly after publication and it completely overhauled the way I thought about language design. I'm currently intermittently working on a language based on this concept, as an environment to create languages that compile to LLVM bytecode to complement Racket's environment to create languages that compile to untyped lambda calculus

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

This is beautiful. I especially like how the type environments naturally arise from lexical scope during macro expansion.

The fact that this composes all the way up from simply typed lambda-calculus to F-omega is pretty impressive.

Doesn't Typed Racket work on the same basis?

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.

Ok, that is rather cool. Could something like this be used to make a better Template Haskell?

Someone's working on something like that already https://github.com/lexi-lambda/hackett

Awesome! Nice find.

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.

Can this be used to type check the language used for macro generation too? Like could this be used to implement a typed racket?

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.

How powerful is the type system? Can you do dependent types?

> Can you do dependent types?

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

eli5?

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.