Eliminating dependent pattern matching without K

JESPER COCKX, DOMINIQUE DEVRIESE, FRANK PIESSENS

Research output: Contribution to journalArticle

Abstract

Dependent pattern matching is an intuitive way to write programs and proofs in dependently typed languages. It is reminiscent of both pattern matching in functional languages and case analysis in on-paper mathematics. However, in general, it is incompatible with new type theories such as homotopy type theory (HoTT). As a consequence, proofs in such theories are typically harder to write and to understand. The source of this incompatibility is the reliance of dependent pattern matching on the so-called K axiom – also known as the uniqueness of identity proofs – which is inadmissible in HoTT. In this paper, we propose a new criterion for dependent pattern matching without K, and prove it correct by a translation to eliminators in the style of Goguen et al. (2006 Algebra, Meaning, and Computation). Our criterion is both less restrictive than existing proposals, and solves a previously undetected problem in the old criterion offered by Agda. It has been implemented in Agda and is the first to be supported by a formal proof. Thus, it brings the benefits of dependent pattern matching to contexts where we cannot assume K, such as HoTT.

Original languageEnglish
Pages (from-to)1-42
Number of pages42
JournalJournal of Functional Programming
Volume26
Issue numbere16
DOIs
Publication statusPublished - 30 Aug 2016

Fingerprint Dive into the research topics of 'Eliminating dependent pattern matching without K'. Together they form a unique fingerprint.

Cite this