Been a bit quiet around here for a while, largely on account of travel broadening the mind. Hopefully, come October, the distractions will be fewer and we can just get on with it. Earlier progress is unlikely, what with reports to write, and the odd paper. No meeting this morning, with Thorsten away and the Ashes and such. Last week’s meeting was quite useful, though, so I thought I’d blog a little.
We had a chat about how the elaborator is likely to work. This involved a certain amount of naming-of-parts, so here goes
Framework : the language of parametrised and modular metavariables and definitions in which the state of the elaborator constitutes a valid module; some metavariables are attached to computations which explain how they are to be computed, given sufficient information; these computations are the suspended executions of programs written in…[this may not be a good name, although it does resemble a Logical Framework in character, even if its purpose is not exactly the same]Blah : the language in which elaboration rules are expressed; Blah’s main constructs arecase analysis on the concrete syntax to be elaborated andrefinement of a problem into subproblems; Blah has an evolving on-paper syntax which will translate to a combinator library [a toy prototype can be found here ]Igor : the program which updates the elaborator state in the light of new information, comprising the implementation of theBlah combinators, the substitution-and-scheduling algorithmambulando and various other bits and pieces
The object of defining Blah is to provide a means to explain to ourselves and to others what on earth is going on, and why it might correspond to the typing rules. Indeed, Blah programs correspond to syntax directed typing rules in which the flow of information from conclusion to hypotheses and back has been made explicit.
Now, a key question addressed unsatisfactorily in Epigram 1 is ‘what are the types of metavariables?’. We shall clearly need to have at least the types of the Epigram language, in order to express unknown expressions of a given type, but do we need other stuff as well, in order to facilitate elaboration? What do we need to represent? What does the elaborator deliver? Not just terms, but also telescopes (from signatures and left-hand sides) and programming problem refinements (from right-hand sides).
The latter, James and I handled by extending the type theory with types corresponding to programming problems, constructors ‘return’ and destructors ‘call’: it was important to extend the type theory in this way because we needed programming problems to occur in the motives constructed for the ↞ operator, hence in inductive hypotheses etc. Eliminators are emphatically not ‘meta-level’ notions: we program them, as well as programming with them.
But what about telescopes? We need to be able to say ‘a binder comprises a telescope and a body parametrised over that telescope’. Does this mean we need to add telescopes to the type theory, or just to the framework? My suspicion is that we’ll want them in the theory sooner or later. More anon…