Is Sized Typing for Coq Practical?

TL;DR

This paper introduces CIC*, a sized type theory for Coq that aims to improve termination and productivity checks through type-based methods, but finds practical implementation challenges due to performance issues.

Contribution

It develops CIC*, a sized type theory based on CIC with features for Coq, and implements a size inference algorithm within Coq's kernel for backward compatibility.

Findings

Size inference causes severe performance degradation in Coq

Type-based termination checking is more robust but less practical

Backward compatibility limits the practicality of size inference

Abstract

Contemporary proof assistants such as Coq require that recursive functions be terminating and corecursive functions be productive to maintain logical consistency of their type theories, and some ensure these properties using syntactic checks. However, being syntactic, they are inherently delicate and restrictive, preventing users from easily writing obviously terminating or productive functions at their whim. Meanwhile, there exist many sized type theories that perform type-based termination and productivity checking, including theories based on the Calculus of (Co)Inductive Constructions (CIC), the core calculus underlying Coq. These theories are more robust and compositional in comparison. So why haven't they been adapted to Coq? In this paper, we venture to answer this question with CIC$\widehat{*}$, a sized type theory based on CIC. It extends past work on sized types in CIC with additional Coq features such as global and local definitions. We also present a corresponding size inference algorithm and implement it within Coq's kernel; for maximal backward compatibility with existing Coq developments, it requires no additional annotations from the user. In our evaluation of the implementation, we find a severe performance degradation when compiling parts of the Coq standard library, inherent to the algorithm itself. We conclude that if we wish to maintain backward compatibility, using size inference as a replacement for syntactic checking is wildly impractical in terms of performance.