Type Systems as Macros
March 20, 2017 at 3:30pm
In this talk, I’ll present Turnstile, a Racket DSL for creating typed DSLs. To implement the type system, programmers write type checking rules resembling traditional judgment syntax. To implement the semantics, they incorporate elaborations into these rules.
Turnstile enhances Racket’s DSL-building capabilities to typed languages, exploiting Racket’s macro system in a novel way to simultaneously type check and rewrite a surface program into a target language. It automatically handles features such as type environments and binding, saving programmers the effort of implementing a type checker from scratch. Building a typed language in this manner also yields modular implementations whose rules may be mixed and matched to create other languages.
Finally, I’ll discuss preliminary efforts using Turnstile to build a typed version of Rosette, which requires no changes to the base language. I’m hoping to receive feedback on the design of Typed Rosette, including what kinds of types programmers would find useful in a language like Rosette.
Stephen is a postdoc at Northeastern University. He works with the Racket team (PLT) and is interested in building DSLs and improving the process of doing so.