Gradual dependent types give principled static and dynamic semantics to programs where part of a type or term is missing. By allowing imprecision, gradual dependent types allow for smooth migration of code from untyped or non-dependently typed languages to languages with full dependent types, enabling the programmer run and test their code even when the full type details haven’t been figured out.

This migration is supported by the \textit{gradual guarantees} of Siek et al, which state that replacing part of a program with the \textit{unknown term} $?$ creates no new static or dynamic type errors. The guarantees ensure that, when an error is encountered, the problem is never too few types, but two fundamentally incompatible types.

However, the benefits of gradual dependent types have not been realized, since existing developments have enabled the gradual guarantees at the expense of other desirable properties. Lennon-Bertrand et al show a “fire-triangle” result: no dependently typed language can satisfy all of strong normalization, conservative extension of CIC, and \textit{graduality}, a strengthening of the gradual guarantees. They instead show that any two combinations of these properties is possible, presenting the Gradual Calculus of Inductive Constructions (GCIC). To achieve the gradual guarantees, they either sacrifice decidable type checking or reject some fully static CIC programs.

We fill this gap in the design space with GrInd, a (Gr)adual language with (Ind)uctive types. Unlike existing gradual languages, GrInd has decidable type checking, the gradual guarantees, and conservative extension of CIC. It sacrifices strong normalization and graduality, but keeps the properties that we actually want.

I am Joey Eremondi, a PhD Student at the University of British Columbia.

I do research in Programming Languages and Theory of Computation, particularly with dependent types. My Masters Thesis was on improving error messages for higher order unification. I’ve also co-authored a few papers on reversal-bounded counter automata.

I have an M.Sc in Computing Science from Utrecht University, a B.Sc. Honours in Computer Science, and a B.Sc. 4-year in Mathematics, both from the University of Saskatchewan.

Github: https://github.com/JoeyEremondi/