An Eq instance for non de Bruijn terms January 30, 2015
tl;dr A non-nameless term equipped with a map specifying a de Bruijn numbering can support an efficient equality without needing a helper function. More abstractly, quotients are not just for proofs: they can help efficiency of programs too.
The cut. You’re writing a small compiler, which defines expressions as follows:
type Var = Int
data Expr = Var Var
| App Expr Expr
| Lam Var Expr
Where Var is provided from some globally unique supply. But while working on a common sub-expression eliminator, you find yourself needing to define equality over expressions.