Gradual typing supports imprecise types in the type system, allowing incremental migration from untyped code to typed in the same language. However, the gradualization of dependent types is challenging, as it complicates type checking, introduces more runtime performance overhead, and potentially breaks some crucial properties. The infamous no-go result by Lennon-Bertrand et al. shows that one may only choose two from normalization, graduality, and semantic conservativity, while all of them are important and desirable.

This ongoing work proposes a gradual dependent type theory based on the Martin-Löf type theory, called Partial Gradual Dependent Type Theory, which is an attempt to challenge this impossibility. As a trade-off, we impose restrictions on imprecise types to prevent the embedding of untyped lambda calculus. PGTT restricts entirely unknown types and only permits dynamic terms on the type indices. However, it allows us to simplify runtime type checks into type parameter checks and elaborate the surface language into a static, dependently typed language, thereby reducing the performance overhead associated with gradual typing.