I can finally factor out common instructions from the end of the two If legs and prepend them to the If's continuation. This wouldn't be an interesting achievement if it wouldn't be written in Ωmega's type-pedantic fragment. To wit:
- tailMerge False [If [Dup]l [Dup]l, Print]l (revThrist' [Dup]l) (revThrist' [Dup]l) [Print]l
- becomes: [(PopN 1v),Dup,Print]l : forall a (b:Prod *0).Thrist Cat [Bool,a; b]sh [a; b]sh
The funny thing is that all the types of values that are on the stack are painstakingly tracked, and the transformation is automatically type correct in Cat because it is type checked in the metalanguage.
I am sure that similar transformations have been proven type correct (and thus pretty correct) before, however I would like to know whether this particular optimization has been already formalized using expressive types.
The big surprise for me was the fact that writing down the transformation only needed a dozen lines of code, support functions included. Of course, my proof of concept only matches on Dup instructions, but the rest is basically boilerplate.
The second surprise is, that so far I did not need a single theorem declaration, an indication that either I am still in very shallow waters regarding the power of Ωmega's typechecker, or my Thrist construction is so clever that it provides enough type hints to the narrowing engine to deduce all types.
I am in the process of writing a paper on all this, and - as always - need some encouragement. Tail merging will definitely belong to the beef part of it.