i have been interested in the use of ABT's to deal with variables and abstraction in a lambda calculus based language. https://semantic-domain.blogspot.com/2015/03/abstract-binding-trees.html provides a helpful introduction for the unfamiliar. one of the questions that i am interested in but havent yet been able to drum up any answers for is: when does the ABT make itself valuable, and are there contexts where it would be beneficial to transform an ABT based tree to a simple AST or vice versa? the initial context this came up to me is in a hypothetical language that, like haskell, has a distinct frontend syntax and a "core" syntax, an explicitly typed, desugared calculus that provides a stable base for the various language extensions to build on. it is my understanding that generally, the frontend haskell syntax is renamed to avoid capture, and thus most operations on the core syntax don't require this information to be tracked (although i do note that GHC does have the code to perform capture avoiding substitution on core expression trees). my question is, if a language uses an ABT, would it be possible to "save work" by implementing the frontend syntax in a traditional AST style, desugar to an ABT, and substitute away? or vice versa, if the frontend is implemented with an ABT, all typechecking and such is performed then, desugaring to an AST? in a way, i guess part of my question is contingent on a related question: during what set of compiler operations is capture avoiding substitution relevant? typechecking and evaluation are obvious ones, but what about implementing optimizations on a reduced core expression language? is there a "sweet spot" for where an ABT adds value in the compiler pipeline, or is it something that's better to go "all in" on?