Abstract

The definition of type equivalence is one of the most important design issues for any typed language. In dependently-typed languages, because terms appear in types, this definition must rely on a definition of term equivalence. In that case, decidability of type checking requires decidability for the term equivalence relation.

Almost all dependently-typed languages require this term equivalence relation to be decidable. Some, such as Coq, Epigram or Agda, do so by employing analyses to force all programs to terminate. Conversely, others, such as DML , ATS, Omega, or Haskell, allow nonterminating computation, but do not allow those terms to appear in types. In both cases, decidable type checking comes at a cost, in terms of complexity and expressiveness.

Conversely, the benefits to be gained by decidable type checking are modest. Termination analyses allow dependently typed programs to verify total correctness properties. However, decidable type checking is not a prerequisite for type safety—and, in this context, type safety implies a weak form of correctness. Furthermore, decidability does not imply tractability. A decidable approximation of program equivalence may still not be useful in practice.

Therefore, we take a different approach: instead of a fixed, decidable, notion for term equivalence, we parameterize our type system with an abstract relation that is not necessarily decidable. We then design a novel set of typing rules that require only weak properties of this abstract relation in the proof of the preservation and progress lemmas. This design provides flexibility: we compare valid instantiations of term equivalence which range from beta-equivalence, to contextual equivalence, to some exotic equivalences.

This is joint work with Joint work with Limin Jia, Zianzhou Zhao, and Vilhelm Sjoberg.