| Abstract Observational Equality, Now! (2008) | |||||||||||||||||
Abstract | |||||||||||||||||
| This paper has something new and positive to say about propositional equality in programming and proof systems based on the Curry-Howard correspondence between propositions and types. We have found a way to present a propositional equality type • which is substitutive, allowing us to reason by replacing equal for equal in propositions; • which reflects the observable behaviour of values rather than their construction: in particular, we have extensionality— functions are equal if they take equal inputs to equal outputs; • which retains strong normalisation, decidable typechecking and canonicity—the property that closed normal forms inhabiting datatypes have canonical constructors; • which allows inductive data structures to be expressed in terms of a standard characterisation of well-founded trees; • which is presented syntactically—you can implement it directly, and we are doing so—this approach stands at the core of Epigram 2; • which you can play with now: we have simulated our system by a shallow embedding in Agda 2, shipping as part of the standard examples package for that system [21]. Until now, it has always been necessary to sacrifice some of these aspects. The closest attempt in the literature is Altenkirch’s construction of a setoid-model for a system with canonicity and extensionality on top of an intensional type theory with proof-irrelevant propositions [4]. Our new proposal simplifies Altenkirch’s construction by adopting McBride’s heterogeneous approach to equality [19]. | |||||||||||||||||
Publication details | |||||||||||||||||
| |||||||||||||||||