being the beginnings of at least zero typecheckers

At Strathclyde, we're always experimenting with the design of type theories. These experiments would be much more fun if they were cheap to implement, so this project is intended to produce a forkable pile of code that can readily be adapted to variations. How much we can do "in software" by reconfiguration and how much by tinkering with the codebase remains to be seen. In trying to support diversity, we've made some mildly deviant design choices.

We make a syntactic separation between "terms" (S,T,s,t) and "eliminations" (E,F,e,f). The latter embed in the former, silently in the concrete syntax, but we underline e for the term made by embedding e when we're working metatheoretically. Apart from embedded eliminations, terms are canonical forms. Eliminations are things which would deliver terms if only they could compute further: they always take the form of a "head" with a spine of terms waiting to apply, and the head is either a variable (in which case the elimination is stuck) or a "cut", t:T (in which case computation may continue). The term t:T computes to t, meaning that the cut has achieved its computational potential and been eliminated. A normal form is cut-free. We expect to be able to synthesize the type of an elimination: its head is either typed in the context or typed explicitly, and every type we can arrive at by successive eliminations is in some way accounted for by that head type. However, we expect only to check the types of terms (with respect to types, which are themselves terms). Moreover, we do not expect that a given term will have at most one type. Our syntactic choices make it easy to be sure that there is always a type around when a term might need to be checked. This reduces the extent to which terms must contain type information (e.g., type annotations on lambdas).

We don't need our syntax to be pretty. It's for kernel theories into which prettier languages might one day elaborate. We do, however, aim to fix a single syntax which is good for multiple theories. Bidirectionality frees us to adopt a sixty-year-old solution to this problem (see XKCD 297). We're pretty much just doing LISP. OK, not quite. Terms are built from atoms and pairing...and lambda and embedded eliminations: concrete things are distinguished from computations which yield them; variables are not atoms (they're de Bruijn indices); there is no code introspection as-of-right. However, we might certainly become interested in type theories where syntaxes replace datatypes as the underlying concrete stuff, at which point we should want cheap reification of computations as constructions (how do you look under a binder? substitute a constructor for the bound variable). For the moment, though, the point is that we have a cheap flexible syntax for both types and terms. We will have rules which say which lumps of syntax happen to be types and which lumps of syntax those types accept. We make new type theories by choosing new judgment forms and new rules, not new syntax.

The basic interaction mode is batch mode. You send in a file, you get back a new version of your file. The machine is like a critical collaborator in a shared project. Diagnostic responses and updates arising from requests are communicated in the output, not via error messages. The process is idempotent: if you feed the machine's output back to itself, it hasn't anything to add or take away. It's not hard to turn this into an interactive process if your editor is half way customizable. The fun part will be making it incremental, so that the machine responds quickly to small patches. This model requires that we preserve the layout of the input as faithfully as possible in the output, so we need front end kit which finds structure on the input without throwing the input away.