The Foil: Capture-Avoiding Substitution With No Sharp Edges

TL;DR

The paper introduces 'The Foil', a type-safe, compile-time enforced technique for capture-avoiding substitution in compilers, improving safety without runtime costs.

Contribution

It extends the rapier technique with Haskell's type system to ensure invariants are maintained statically, reducing bugs.

Findings

The Foil prevents capture-related bugs through static type guarantees.

It achieves this without incurring runtime overhead.

The approach simplifies compiler correctness by enforcing invariants at compile time.

Abstract

Correctly manipulating program terms in a compiler is surprisingly difficult because of the need to avoid name capture. The rapier from "Secrets of the Glasgow Haskell Compiler inliner" 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.