Turnstile+: Dependent Type Systems as Macros

In 2017, a team from Northeastern University released Turnstile, a framework for implementing propositionally typed languages in Racket; cf. naasking's story Type Systems as Macros. The system was really nice because it allowed type systems to be expressed in a manner similar to the way theoretical PL researchers would in a paper, and because it hooked into Racket's clean compiler backend.

Now Stephen Chang, one of that team, together with new coauthors Michael Ballantyne, Usamilo Turner and William Bowman, have released a rewrite that they call Turnstile+, together with a POPL article, Dependent Type Systems as Macros. From that article's introduction:

Turnstile+ represents a major research leap over its predecessor. Specifically, we solve the major challenges necessary to implement dependent types and their accompanying DSLs and extensions (which Turnstile could not support), while retaining the original abilities of Turnstile. For example, one considerable obstacle was the separation between the macro expansion phase and a program’s runtime phase. Since dependently typed languages may evaluate expressions while type checking, checking dependent types with macros requires new macrology design patterns and abstractions for interleaving expansion, type checking, and evaluation. The following summarizes our key innovations.

  • Turnstile+ demands a radically different API for implementing a language’s types. It must be straightforward yet expressive enough to represent a range of constructs from base types, to binding forms like Π-types, to datatype definition forms for indexed inductive type families.
  • Turnstile+ includes an API for defining type-level computation, which we dub normalization by macro expansion. A programmer writes a reduction rule using syntax resembling familiar on-paper notation, and Turnstile+ generates a macro definition that performs the reduction during macro expansion. This allows easily implementing modular type-level evaluation.
  • Turnstile+’s new type API adds a generic type operation interface, enabling modular implementation of features such as error messages, pattern matching, and resugaring. This is particularly important for implementing tools like tactic systems that inspect intermediate type-checking steps and construct partial terms.
  • Turnstile+’s core type checking infrastructure requires an overhaul, specifically with first-class type environments, in order to accommodate features like dependent binding structures of the shape[x:τ]...,i.e., telescopes [de Bruijn 1991; McBride 2000].
  • Relatedly, Turnstile+’s inference-rule syntax is extended so that operations over telescopes, or premises with references to telescopes, operate as folds instead of as maps

The code is available at https://github.com/stchang/macrotypes.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Macros again

It does bother me to see folks continuing to further invest in macros; I see practical reasons why they do it (just as I see practical reasons why physicists keep investing in string theory), but I don't see that understanding makes it any more laudable. For fexprs to catch up, though, they need to be competing; and for my part, I'm type-skeptical. I don't recall (perhaps it's slipped my mind?) attempting to explain on LtU my beef with types.

(1) These sorts of type systems have to support all correct formal reasoning that can be done. Gödel's theorems aren't friendly to that. I've wondered for a couple of decades or so, if the root of this is some sort of mis-step in setting up the problem. Viciously circular logic is an existential crisis, whereas the equivalent computation is just a program that's hung up in an infinite loop (it happens); is there a way, by embedding logical reasoning within the computational system (rather than vice versa), to bleed off the antinomies into mere non-halting computation? It's apparently impossible to prove (formally) this can't be done, because it involves stepping outside the rules; yet there's also no knowing that it can be done except to figure out how.

(2) Typing and computation put conflicting demands on programming-language design. Typing is formal proof about static expressions. Computation is what those static expressions actually do when evaluated. When you design a language to support typing, you're trying to make clear how the formal proof works. When you design a language to support computation, though, you're trying —as your first line of defense against getting the program wrong, before you even begin to reason formally about it— to make clear what the program does. If you can't tell, by looking at the program, what it does, that's a non-starter. And I suggest you cannot successfully design for both at once. Designing to clarify the formal reasoning obfuscates the algorithm; designing to clarify the algorithm obfuscates the formal reasoning.

on the goal of clear computation

Programmers will certainly write code I cannot understand. For example, see the procmail source code. Seems to be perfect, right?

Programmers, like human writers in other fields, are also bad and biased judges of whether their own code is 'clear'. They know what they meant, which interferes with reading what was actually written. An independent review is required to effectively judge clarity.

Even when each unit of code is written clearly, it can become a challenge to comprehend after we layer dependency upon dependency until we have a dense forest of code. Further, there are software packages and team development. Even if you read and understand what a program does today, it might subtly change tomorrow, and perhaps you won't find the time or motivation to again 'look at the program' to understand the change and 'tell what it does'. If by accident you depend on some implementation detail that changes, behavior may break without obvious, traceable, or easily isolable reason.

I'm curious how you would propose to "design for" clarity. I believe we could try to build a culture of clarity. But having spoken to programmers who insist "comments trigger me" and insist on naming functions based on numbers in a separate document, I have some doubts that any culture would be stronger than the ego of programmers who insist they know what they're doing.

Types are not perfect, but they seem rather practical in a world where clear communication is difficult to scale beyond one programmer writing to a near-future self.