Type Systems as Macros

• PDF
• Year: 2017
• Authors
  • Stephen Chang
  • Alex Knauth
  • Ben Greenman
• Links
  • Turnstile
  • type system
  • bidirectional typing
  • Racket

Context

This is one of my favourite papers because it’s such a great hack, and reminds me of a bunch of statics-as-macros style tricks that we used in Witchcraft. I need to double check this, but IIRC this is also how [[core.typed]] was implemented in Clojure.

Abstract

Abstract

We present TURNSTILE, a metalanguage for creating typed embedded languages. 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 critically depends on the idea of linguistic reuse. It exploits a macro system in a novel way to simultaneously type check and rewrite a surface program into a target language. Reusing a macro system also yields modular implementations whose rules may be mixed and matched to create other languages. Combined with typical compiler and runtime reuse, TURNSTILE produces performant typed embedded languages with little effort.

Notes

Quote

we really don’t want to build a programming language from scratch … better, let’s inherit the infrastructure of some other language

— Paul Hudak

• A macro system runs early in the compilation process
  • This is also where type systems tend to run in the compilation pipeline.
• Interleaved type checking and rewriting
• Much emphasis on good error messages
• Can use macros to reuse parts of the parent type system
• They don’t show it explicitly in the paper, but mention that one could use this to define an effect system.

Turnstile

Turnstile is a metalanguage that has Bidirectional typing, though with different syntax that you often see elsewhere:

Turnstile	Meaning	Pfenning
$\Leftarrow$	Check	$\uparrow$
$\Rightarrow$	Synthesise	$\downarrow$
$e\gg e^{\prime }$	$e$ expands to $e^{\prime }$	N/A

$$\frac{x\gg \bar{x}:\tau \in \Gamma }{\Gamma ⊢x\gg \bar{x}:\tau }\text{TE-Var}$$ $$\frac{\Gamma ,x\gg \bar{x}:{\tau }_1⊢e\gg \bar{e}:{\tau }_2\bar{x}\ne e}{\Gamma ⊢\lambda x:{\tau }_1.e\gg \lambda \bar{x}.\bar{e}:{\tau }_1\to {\tau }_2}\text{TE-Abs}$$ $$\frac{\Gamma ⊢e_1\gg {\bar{e}}_1:{\tau }_1\to {\tau }_2\Gamma ⊢e_2\gg {\bar{e}}_2:{\tau }_1}{\Gamma ⊢e_1{e}_2\gg {\bar{e}}_1{\bar{e}}_2:{\tau }_2}\text{TE-App}$$

They go further to include existentials, kindedness, and higher order polymorphism akin to System $F_{\omega }$.