Rabe F (2021)
Publication Type: Conference contribution
Publication year: 2021
Publisher: Springer Science and Business Media Deutschland GmbH
Book Volume: 12833 LNAI
Pages Range: 211-227
Conference Proceedings Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Event location: Virtual
ISBN: 9783030810962
DOI: 10.1007/978-3-030-81097-9_18
In soft type systems terms and types exist independently and typing is a binary relation between them. That allows the same term to have multiple types, which is in particular the case in the presence of subtyping. Thus, a soft type system may define equality in such a way that two terms can be equal at one type but unequal at another type. We explore the design of soft type systems with such a type-dependent equality. The most promising application is that it yields a more natural treatment of quotient types: if two terms can be different at the base type but equal at the quotient type, we can use the same representation in both types without incurring the cost of using equivalence classes. That can help formalize mathematics, where the official definition of quotients uses equivalence classes but practical notations usually do not. The main drawback of such a system is that the substitution of equals by equals becomes more complex as it now depends on the type with which the equal terms are used. We analyze the general problem, show examples from major soft-typed proof assistants, and then present a simple language that allows studying type-dependent equality in a simple rigorous setting.
APA:
Rabe, F. (2021). A Language with Type-Dependent Equality. In Fairouz Kamareddine, Claudio Sacerdoti Coen (Eds.), Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (pp. 211-227). Virtual: Springer Science and Business Media Deutschland GmbH.
MLA:
Rabe, Florian. "A Language with Type-Dependent Equality." Proceedings of the 14th International Conference on Intelligent Computer Mathematics, CICM 2021, Virtual Ed. Fairouz Kamareddine, Claudio Sacerdoti Coen, Springer Science and Business Media Deutschland GmbH, 2021. 211-227.
BibTeX: Download