5
$\begingroup$

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!

$\endgroup$
  • $\begingroup$ Why do you believe that? You say it "removes the isolation between types and code"; why would that be different for primitive recursion? Have you tried proving either direction? $\endgroup$ – Raphael Feb 18 '16 at 7:34
  • $\begingroup$ I think the implication was "removes the isolation between types and code [and code might not be strongly normalizing]" but I could be wrong as to the intentions of that statement. $\endgroup$ – Jake Feb 18 '16 at 20:44
3
+50
$\begingroup$

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 weather it was definitional equal to another expression. Because of the way we define definitional equality in most cases this demands evaluation. The calculus of constructions is actually strongly normalizing. Type checking of CoC is decidable and requires no termination checking. But to make this theory more useful we want to add inductive types and recursion over these inductive types (thus we get the calculus of inductive constructions which Coq is based on). You can view this as a means of adding terms to our language that add computational content not otherwise present. Note than many inductive types can already be represented in CoC without aide but CoC can't represent everything CoIC can. Coq and Agda both have termination checkers that except all primitive recursive functions and can both encode the Ackermann function as well. You can see more about this in a question I once asked here.

good refrences on Agda's termination checker: 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 the state of the art in mainstream implementation (at least as far as I am aware).

$\endgroup$
4
$\begingroup$

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.

$\endgroup$

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.