This is part II of a series of blog posts, but I don't know if part I or part III is as immediately relevant to us.
One of the things this touches on is associating expressions with source code. That's something I tend to neglect to do, but this makes it look easy.
The other thing is it shows a way to normalize expressions to other expressions, just using HOAS (aka putting functions in your expression AST). This makes expressions the only run time data structures needed in the language.
Normalization of expressions is commonly needed in dependent type theories because it makes it possible to compare types by intensional (implementation) equality, even if those types contain program expressions. (Comparing types for equality is needed for instance when typechecking a funtcion application, since you might have used an argument of incorrect type.)
