Excellent answer! Splitting the Symantics class into pieces is one of the techniques that we didn't need for solving the original problem (tagless partial evaluation without resorting to fancy types) that set us on this track. Which is too bad, because it would have made a nice addition. The 'typecase pattern', on the other hand, was one of the explicit techniques we did use. One of these days, Oleg, Ken and I need to write a follow-up on this, as the code contains a number of extra techniques (in the advanced partial evaluation parts) which were not explained in our paper. And, of course, Oleg's added a number of refinements to the general technique [see his web site]. I must admit that I find it amusing that most people seem to use finally-tagless for writing interpreters, while we created it for partial evaluation and program transformation! [It also allows you to do certain kinds of program analyses, but one needs additional techniques to make that comfortable - another thing to write up properly]. Jacques