5
$\begingroup$

So from reading "Advanced Topics in Types and Programming Languages" (ATTPL) I know of the calculus of constructions (CoC). It also presents the "algorithmic" type checking rules. Reading Coq's documentation on the Calculus of Inductive Constructions (CioC) you can get a sense of things but it is far from algorithmic. Is there any reference on algorithmic type checking for CioC?

$\endgroup$
4
$\begingroup$

The problem of giving an algorithmic reading to the typing rules in CIC, and dependent type systems in general, is quite subtle.

One recommendation is Randy Pollack's Typechecking in Pure Type Systems, Gille Barthe's Type Checking *Injective Pure Type Systems and McKinna and Pollack's Pure Type Systems formalized.

The first basic idea is to "push" the conversion rule $$ \frac{\Gamma \vdash t: A\quad A\simeq B}{\Gamma\vdash t : B}$$

into the application rule $$ \frac{\Gamma \vdash t:A\quad \Gamma\vdash u:A' \quad A\simeq \Pi x: A'.B}{\Gamma\vdash t\ u:B\{x\mapsto u\}}$$

And similarly for "application-like" rules. The theorem is that these modified rules suffice for type-checking (without conversion), with the exception of a possible single application of conversion at the end.

This makes the rules type-directed, which allows a straightforward implementation. There are additional shortcuts which allow skipping verification of $\mathrm{WF}$, for example, if it is known that it is going to be derived later, or it is admissible.

As Luke notes, there is no complete treatment of such shortcuts, and the validity of these is sometimes quite complicated to prove (e.g. the "expansion postponement" rule).

Checking conversion of terms with $\delta$-reductions (defined functions) is a whole bag of worms: when checking

$$ f\ t_1\ldots t_n\simeq f\ u_1\ldots u_n$$

should you just check $t_i\simeq u_i$ for each $i$, or unfold $f$? The answer is, unsurprisingly, it depends. In general clever heuristics are used, e.g. "unfold $f$ if it is a projection, otherwise try checking equivalence of the arguments, and unfold $f$ if that fails".

$\endgroup$
3
$\begingroup$

The page you link has a series of references just before Section 4.1, and you can't really get better than these.

The inference rules are also given in section 4.2, but for me the formatting seems to have gone haywire, so they're a bit hard to read. Assuming you're comfortable with CoC or $\lambda$-calculus, it should be clear that these give the algorithm (if you're not, then jumping into CoIC or pCoIC may be a bit of an uphill struggle).

Maria João Frade has made some lecture slides available which goes through it with a bit more explanation (the CoIC part is the second section of the slides).

Ultimately though, Bertot and Castéran's book is probably the best reference for understanding CoIC, unless you want to slog through the research papers (having partially done the latter, it's not impossible).

$\endgroup$
  • $\begingroup$ Have you seen the distinction between algorithmic type checking and non-algorithmic type checking? Think about how you would implement these rules. For instance say I have a construction $a : \forall y, y = y$ and another $f : (\forall x, x = x) -> P$. Clearly $f a : P$ but yet the typing rules don't talk quite exactly about how to handle such cases. This is mentioned in algorithmic type checking. Additionally there is nondeterminism in these rules. Take the rules for concluding $WF$, for a given instance of $WF(E)[\Gamma]$ multiple rules might apply. Algorithmic type checking solves this. $\endgroup$ – Jake Apr 10 '15 at 1:45
  • $\begingroup$ @Jake, what I was attempting to say is that the references available are not great, and that you can glean some things from freely available references, but the best bet is getting Bertot and Casteran. $\endgroup$ – Luke Mathieson Apr 10 '15 at 2:22

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.