We Need Real Tools for Generating Type

For decades programmers have had access to production-quality tools for generating lexers and parsers from high-level declarative specifications. Recent work on nano-pass compiler frameworks [3] makes it possible to develop a many-pass compiler using a grammar-based domain-specific language. Yet we still do not have mature, flexible tools for generating efficient type checkers and type inferencers from a high-level description (ideally, directly from the typing judgements). Although researchers use logic programming, term writing, and proof assis-tants to express type systems in a declarative fashion, in practice developers— including computer science researchers—write production type inferencers and type checkers by hand using general-purpose programming languages. This point was driven home for one of us during development of the compiler for Harlan [2] (a language for high-level GPGPU programming). After defining the type system for Harlan’s region-based memory management system, we wanted to generate a type inferencer from the typing judgements. We knew of no too