Summary
Programs sometimes rely on assumptions called postulates that say certain data exists without showing it, but this can cause problems if the program gets stuck and can’t continue running. The authors explore how to safely use these assumptions when some parts are erased (ignored during program running) and when dealing with proofs that two things are equal. They show how certain 'quotient types' which group things by an equivalence can be handled safely with erased postulates, allowing programs to run without getting stuck. They also study when it’s okay to use special conversions based on erased equality proofs and explain limits when dealing with more complex assumptions like univalence. Their results are supported by verified proofs in the Agda programming language.
type theoryerased postulatesidentity typesquotient typesequivalence classesprogram safetytransport (casting)equality reflectionunivalenceAgda proofs
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.