Google Research

The Foil: Capture-Avoiding Substitution With No Sharp Edges

  • Adam Paszke
  • Alexey Radul
  • Dougal Maclaurin
Symposium on Implementation and Application of Functional Languages (IFL 2022) (2022)

Abstract

Correctly manipulating program terms in a compiler is surprisingly difficult because of the need to avoid name capture. The rapier from Peyton Jones and Marlow [8] is a cutting-edge technique for fast, stateless capture-avoiding substitution for expressions represented with explicit names. It is, however, a sharp tool—its invariants are tricky and need to be maintained throughout the whole compiler that uses it. We describe the foil, an elaboration of the rapier that uses Haskell’s type system to enforce the rapier’s invariants statically, preventing a class of hard-to-find bugs, but without adding any run-time overheads.

Research Areas

Learn more about how we do research

We maintain a portfolio of research projects, providing individuals and teams the freedom to emphasize specific types of work