New equations for neutral terms : a sound and complete decision procedure, formalized

Allais, Guillaume and McBride, Conor and Boutillier, Pierre; (2013) New equations for neutral terms : a sound and complete decision procedure, formalized. In: DTP '13: Proceedings of the 2013 ACM SIGPLAN workshop on Dependently-typed programming. ACM, New York, pp. 13-24. ISBN 9781450323840 (https://doi.org/10.1145/2502409.2502411)

[thumbnail of Allais-etal-DTP2013-New-equations-for-neutral-terms]
Preview
 Text. Filename: Allais_etal_DTP2013_New_equations_for_neutral_terms.pdf
Accepted Author Manuscript
License: Strathprints license 1.0
Download (860kB)| Preview

Abstract

The definitional equality of an intensional type theory is its test of type compatibility. Today's systems rely on ordinary evaluation semantics to compare expressions in types, frustrating users with type errors arising when evaluation fails to identify two `obviously' equal terms. If only the machine could decide a richer theory! We propose a way to decide theories which supplement evaluation with `ν-rules', rearranging the neutral parts of normal forms, and report a successful initial experiment. We study a simple λ-calculus with primitive fold, map and append operations on lists and develop in Agda a sound and complete decision procedure for an equational theory enriched with monoid, functor and fusion laws.

ORCID iDs

Allais, Guillaume ORCID logoORCID: https://orcid.org/0000-0002-4091-657X, McBride, Conor ORCID logoORCID: https://orcid.org/0000-0003-1487-0886 and Boutillier, Pierre;
CORE (COnnecting REpositories)