To recap, my current project is designing and implementing a type theory similar to LF. Much like LF, it admits representations of deductive systems and derivations in such systems. The idea is to jigger the theory up so that much of the internal structure of these represenations doesn't actually need to be written down. (or, in the case of the implementation, doesn't need to be stored in memory) This is because a typical LF "program" is wildly redundant in many predictable ways.
So, you predict them, analyze them, and get rid of them. The theory was somewhat of a pain to work out, but let me tell ya, the implementation work is a pain in the ass so big, I think I will have to grow another several dozen asses just to accomodate its bulk.
This morning, I ran the code that takes an existing twelf program, and "compresses" it, that is, translates it into my crazy new LF-variant. This code is fairly well tested by now. It runs quietly, over about 3,000 LF declarations, and finishes.
The part that still isn't working is the type checker, annoyingly enough, which I wrote much, much eariler, and theoretically ought to be much more perfect. "Just as a sanity check", I tell myself, I make sure that M* : A* for every M* that's a translation of M, and every A* that's a translation of A, where originally M : A. Of course this preservation of well-typedness should hold. This guarantee is practically what all the theory is for, really.
Oh, but it doesn't. Right from the very beginning there were bugs, and each time I fixed one, the number of declarations that checked correctly would pop up a bit, sometimes by a factor of two or three or ten. Those were good times.
Today was less encouraging.
Today I started out knowing that declaration number 2,476 out of about 3,000 didn't typecheck right. I figured, I just might be done today. I might just fix this one and have, at a first approximation, a correct program. One that at least conquered the rather large first testing corpus I threw at it.
A couple of hours of debugging revealed that I was simply failing to carry out an instantiation of a solved existential variable, because I had unconservatively misanalyzed under what circumstances I needed to do so. Added like two functions, and one case to another, and that case worked fine.
I ran the full test again. Oh, bother. Another bug. This one looked a lot bigger, a lot deeper. Deep in the guts of dark, sinister, deBruign-indexed explicit substitution munging.
On declaration number 2,477 out of about 3,000, the very next one. ARG.
