The payoff is that I finally fucking got LF-to-LF* translation working in some capacity. It was shamefully reasonable to code up, considering how long I've been whinging about how confusing it was. The downside is that it's still quite ugly. There is one translation from twelf internal syntax to my custom syntax datatype, and a second pass that actually does the compression, taking into account crap that is to be left in an imperative list in some stupid top-level structure that I created just for that purpose. Grah.
Tom7 said to me last night that he knows of no major features he feels missing from ML as a language, that apart from syntactic quibbles and maybe the absence of a nice macro system, it's all the tool he needs. In contrast, and I admit this may be in part because I'm simply not as experienced and as talented a programmer, coding runs like this one give me the programming-language equivalent of groping for words in a natural language. No matter how hard I tried to say what I wanted to say, it came out all stupid and hackish. Maybe I would have been considerably happier if I had record-type row variables. I'm willing to consider that it's UI issues to a large degree as well. At the end of the day I have a zillion theories, actually. My cup runneth over with reasons that I dread programming. I really want to eliminate that dread, and I don't know how.