Inside 245-5D

Existential Pontification and Generalized Abstract Digressions

January, 2015

An Eq instance for non de Bruijn terms

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 […]

  • January 30, 2015