Even if there is only a single "concrete" interpretation of syntax (i.e. as generated SSA code), it still enables implementation of code transformers like autodiff, and lifting expressions over complex numbers. I wrote a unification algo in scheme before. Don't remember where I left it.. I have to this from the ground up once, to see the connections, then solve it..