License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2019.2
URN: urn:nbn:de:0030-drops-130666
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2020/13066/
Go to the corresponding LIPIcs Volume Portal

Cockx, Jesper

Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules

pdf-format:
LIPIcs-TYPES-2019-2.pdf (0.6 MB)

Abstract

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 - such as strictly positive datatypes, complete case analysis, and well-founded induction - 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.

BibTeX - Entry

@InProceedings{cockx:LIPIcs:2020:13066,
  author =	{Jesper Cockx},
  title =	{{Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules}},
  booktitle =	{25th International Conference on Types for Proofs and Programs (TYPES 2019)},
  pages =	{2:1--2:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-158-0},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{175},
  editor =	{Marc Bezem and Assia Mahboubi},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/opus/volltexte/2020/13066},
  URN =		{urn:nbn:de:0030-drops-130666},
  doi =		{10.4230/LIPIcs.TYPES.2019.2},
  annote =	{Keywords: Dependent types, Proof assistants, Rewrite rules, Higher-order rewriting, Agda}
}

Keywords: Dependent types, Proof assistants, Rewrite rules, Higher-order rewriting, Agda
Collection: 25th International Conference on Types for Proofs and Programs (TYPES 2019)
Issue Date: 2020
Date of publication: 24.09.2020
Supplementary Material: The official documentation of rewrite rules in Agda is available in the user manual at https://agda.readthedocs.io/en/v2.6.1/language/rewriting.html. The full source code of Agda (including rewrite rules) is available on Github at https://github.com/agda/agda/.

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI