Decidability of dependent typing on primitive recursive languages

Question

With a dependent type system in a normal functional language type checking may never halt. This is partially because dependent typing removes the isolation between types, and code. My question is this: would an implementation of dependent typing for a primitive recursive language(not Turing-complete) be guaranteed to halt? Thanks!

Answer 1

Not only is the answer to this question yes, but this is exactly the strategy that modern implementations like Coq and Agda take! To be precise, the type checker has to preform evaluation when deciding definitional equality so it would, if given the right language, be possible to write an infinite loop and ask whether a term was definitionally equal to another term. Because of the way we define definitional equality in most cases, this demands evaluation.

The calculus of constructions (CoC) is actually strongly normalizing. Type checking of CoC is decidable and requires no termination checking. But to make this theory more useful, we add the ability to define inductive types and recursions over them. This way, we get the calculus of inductive constructions (CIC), which Coq is based on. You can view this as a means of adding terms to our language which add computational content that would otherwise not be present.

Note than many inductive types can already be represented in CoC without the aid of CIC, but CoC cannot represent everything CIC can. Coq and Agda both have termination checkers which accept all primitive recursive functions, and both also allow encoding the Ackermann function. You can see more about this in a question I once asked here on a characterization of the class of primitive recursive functions.

Good refrences on Agda's termination checker are

• http://www2.tcs.ifi.lmu.de/~abel/foetus/
• http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.TerminationChecker

There is also a lot of work on sized types to provide an alternative to termination checking as well as some work on abstract interpretation based solutions. Currently however, checking for a generalization (see Foetus) of primitive recursion is as far as the state of the art in mainstream implementations goes — at least as far as I am aware.

Answer 2

Primitive recursive isn't actually an interesting threshold here. As long as the language only allows terminating programs, and type equality is defined by normal form equality, dependent typing can be checked statically.

The gist of the proof is obvious: if the language only allows terminating programs, then all computations on types terminate, because they're computations in the language. However, there are some subtleties.

One subtlety is that type checking must be defined by syntactic means. If type checking is semantic, all bets are off. For example, consider the program $\lambda x:\mathbb{N}^k. (\mathtt{if} \: D(x) \: \mathtt{then} \: \texttt{"bad"} \: \mathtt{else} \: 0)_{\mathbb{N}}$ where $D$ is a Diophantine equation. If $D$ has no solution then this program will never try to pass off the string $\texttt{"bad"}$ as an integer (type $\mathbb{N}$). If the typing rules are defined by the runtime semantics, this program is well-typed iff the Diophantine equation has no solution, which is an undecidable problem. If the typing rules follow a classic syntactic presentation, then this program is ill-typed, because it requires both branches of the if statement to be well-typed.

Another subtlety lies in the definition of type equality. Type checking requires not only calculating types, but also checking if they're equal (or more generally if one type is a subtype of another). Even if type checking follows syntactic rules, equality could bring back undecidable semantics — consider $(\texttt{make_array}(n,0))_{\texttt{array}(m)}$ (make an array of length $n$, of type array of length $m$): the compiler must be able to decide whether $m$ and $n$ are equal. If $m$ and $n$ are themselves calculated, say as solutions of a Diophantine equation, this could be undecidable.

A third subtlety is that decidable type checking is a lot more common than decidable type inference. Type checking may require a lot of type annotations in the code. Without type annotations, ever relatively weak type systems are undecidable; for example System F, which only has terms depending on types and not types depending on terms, has undecidable type inference (whereas type checking is easy).

All these subtleties are really manifestations of the same underlying concern. If the type checker only needs to calculate terms, then as long as the language only allows terminating programs, the type checker itself is terminating. But if the type system allows expressing more than what the language itself can do — by adding a level of quantification (the property must hold for all possible executions, not just for one execution), by adding a way to compare the semantics of two expressions, or by adding a step of partial reconstruction — then the type system pretty quickly becomes undecidable. The most basic dependently typed version of the lambda calculus, $\lambda\Pi$ in the lambda cube, has a syntactic type system, as do its extensions the calculus of constructions which is the basis of program/proof languages such as Coq.

Languages with a terminating dependent type system generally cope with this problem by requiring sufficient type annotations, and defining a syntactic type system. If the programmer doesn't give enough information to let the compiler conclude that the program is well-typed, then the program is rejected, even though there's still some possibility that it would execute without any type error. This is particularly important in languages where programs are proofs, and well-typed programs are correct proofs.