TY - GEN
T1 - Type Theory Unchained
T2 - 25th International Conference on Types for Proofs and Programs, TYPES 2019
AU - Cockx, Jesper
PY - 2020
Y1 - 2020
N2 - Dependently typed languages such as Coq and Agda can statically guarantee the correctness of our proofs and programs. To provide this guarantee, they restrict users to certain schemes a- such as strictly positive datatypes, complete case analysis, and well-founded induction a- that are known to be safe. However, these restrictions can be too strict, making programs and proofs harder to write than necessary. On a higher level, they also prevent us from imagining the different ways the language could be extended. In this paper I show how to extend a dependently typed language with user-defined higher-order non-linear rewrite rules. Rewrite rules are a form of equality reflection that is applied automatically by the typechecker. I have implemented rewrite rules as an extension to Agda, and I give six examples how to use them both to make proofs easier and to experiment with extensions of type theory. I also show how to make rewrite rules interact well with other features of Agda such as-equality, implicit arguments, data and record types, irrelevance, and universe level polymorphism. Thus rewrite rules break the chains on computation and put its power back into the hands of its rightful owner: Yours.
AB - Dependently typed languages such as Coq and Agda can statically guarantee the correctness of our proofs and programs. To provide this guarantee, they restrict users to certain schemes a- such as strictly positive datatypes, complete case analysis, and well-founded induction a- that are known to be safe. However, these restrictions can be too strict, making programs and proofs harder to write than necessary. On a higher level, they also prevent us from imagining the different ways the language could be extended. In this paper I show how to extend a dependently typed language with user-defined higher-order non-linear rewrite rules. Rewrite rules are a form of equality reflection that is applied automatically by the typechecker. I have implemented rewrite rules as an extension to Agda, and I give six examples how to use them both to make proofs easier and to experiment with extensions of type theory. I also show how to make rewrite rules interact well with other features of Agda such as-equality, implicit arguments, data and record types, irrelevance, and universe level polymorphism. Thus rewrite rules break the chains on computation and put its power back into the hands of its rightful owner: Yours.
KW - Agda
KW - Dependent types
KW - Higher-order rewriting
KW - Proof assistants
KW - Rewrite rules
UR - http://www.scopus.com/inward/record.url?scp=85092787830&partnerID=8YFLogxK
U2 - 10.4230/LIPIcs.TYPES.2019.2
DO - 10.4230/LIPIcs.TYPES.2019.2
M3 - Conference contribution
AN - SCOPUS:85092787830
T3 - Leibniz International Proceedings in Informatics, LIPIcs
BT - 25th International Conference on Types for Proofs and Programs, TYPES 2019
A2 - Bezem, Marc
A2 - Mahboubi, Assia
A2 - Mahboubi, Assia
PB - Schloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Y2 - 11 June 2019 through 14 June 2019
ER -