Type theory advances ensure safe erasure with identity and quotients
Erased Postulates, Identity Types and Quotients
Programming LanguagesLogic in Computer Science
Summary
When programmers use type theory to write programs, they sometimes assume certain facts without giving explicit evidence, called postulates. The authors study how to safely erase these assumptions in the final program without causing it to get stuck or stop working. They show it is safe to do this even when working with concepts that identify things as equal (identity types) and when grouping things into classes (quotients). They also explore limits on safely transporting values using these erased proofs and provide formal machine-checked proofs to back their results.
What this means in practice
- •For programming language designers: Design type systems that safely support erased assumptions and quotient types without risking program failure at runtime.
- •For compiler developers: Implement optimizations that erase proofs and postulates related to identity and quotients while preserving guaranteed program execution.
A theory result. No direct application yet.
Authors
Nils Anders Danielsson
Abstract
This text is concerned with the question of whether, in type theory with erasure annotations, one can postulate that some type is inhabited and still have a guarantee that a program will not get stuck. Previous work has provided such guarantees for consistent erased postulates, i.e. postulates that are restricted to be used in erased contexts. Here those guarantees are extended to type theory with identity types. Similar ideas provide a simple way to support quotient types: it is shown that one can let things like "the equivalence classes for two related values are equal" be erased postulates and have an eliminator that only computes for the equivalence class constructor, and still get a guarantee that programs will compute correctly. Another question is whether programs compute correctly if one is allowed to transport (cast) using erased identity proofs. It is shown that this is safe in the absence of quotients and postulates, and in the presence of quotients and erased postulates that can be implemented using equality reflection. However, unrestricted transports of this kind are not compatible with erased, postulated univalence. For that reason the text includes a study of the function []-cong, which encapsulates a limited form of transport for erased identity proofs. The text is accompanied by machine-checked Agda proofs.