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

Research output: Chapter in Book/Conference proceedings/Edited volumeConference contributionScientificpeer-review

1 Citation (Scopus)
4 Downloads (Pure)

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 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.

Original languageEnglish
Title of host publication25th International Conference on Types for Proofs and Programs, TYPES 2019
EditorsMarc Bezem, Assia Mahboubi, Assia Mahboubi
PublisherSchloss Dagstuhl- Leibniz-Zentrum fur Informatik GmbH, Dagstuhl Publishing
Number of pages27
ISBN (Electronic)9783959771580
DOIs
Publication statusPublished - 2020
Event25th International Conference on Types for Proofs and Programs, TYPES 2019 - Oslo, Norway
Duration: 11 Jun 201914 Jun 2019

Publication series

NameLeibniz International Proceedings in Informatics, LIPIcs
Volume175
ISSN (Print)1868-8969

Conference

Conference25th International Conference on Types for Proofs and Programs, TYPES 2019
CountryNorway
CityOslo
Period11/06/1914/06/19

Keywords

  • Agda
  • Dependent types
  • Higher-order rewriting
  • Proof assistants
  • Rewrite rules

Fingerprint Dive into the research topics of 'Type Theory Unchained: Extending Agda with User-Defined Rewrite Rules'. Together they form a unique fingerprint.

Cite this