Approximate normalization for gradual dependent types
Résumé
Dependent types help programmers write highly reliable code. However, this reliability comes at a cost: it canbe challenging to write new prototypes in (or migrate old code to) dependently-typed programming languages.Gradual typing makes static type disciplines more flexible, so an appropriate notion of gradual dependenttypes could fruitfully lower this cost. However, dependent types raise unique challenges for gradual typing.Dependent typechecking involves the execution of program code, but gradually-typed code can signal runtimetype errors or diverge. These runtime errors threaten the soundness guarantees that make dependent types soattractive, while divergence spoils the type-driven programming experience.This paper presents GDTL, a gradual dependently-typed language that emphasizes pragmatic dependently-typed programming. GDTL fully embeds both an untyped and dependently-typed language, and allows forsmooth transitions between the two. In addition to gradual types we introducegradual terms, which allow theuser to be imprecise in type indices and to omit proof terms; runtime checks ensure type safety. To accountfor nontermination and failure, we distinguish between compile-time normalization and run-time execution:compile-time normalization isapproximatebut total, while runtime execution isexact, but may fail or diverge.We prove that GDTL has decidable typechecking and satisfies all the expected properties of gradual languages.In particular, GDTL satisfies the static and dynamic gradual guarantees: reducing type precision preservestypedness, and altering type precision does not change program behavior outside of dynamic type failures. Toprove these properties, we were led to establish a novelnormalization gradual guaranteethat captures themonotonicity of approximate normalization with respect to imprecision