Preprint
Simulating Large Eliminations in Cedille
ArXiv.org
12/14/2021
DOI: 10.48550/arxiv.2112.07817
Abstract
Large eliminations provide an expressive mechanism for arity- and
type-generic programming. However, as large eliminations are closely tied to a
type theory's primitive notion of inductive type, this expressivity is not
expected within polymorphic lambda calculi in which datatypes are encoded using
impredicative quantification. We report progress on simulating large
eliminations for datatype encodings in one such type theory, the calculus of
dependent lambda eliminations (CDLE). Specifically, we show that the expected
computation rules for large eliminations, expressed using a derived type of
extensional equality of types, can be proven within CDLE. We present several
case studies, demonstrating the adequacy of this simulation for a variety of
generic programming tasks, and a generic formulation of the simulation allowing
its use for any datatype. All results have been mechanically checked by
Cedille, an implementation of CDLE.
Details
- Title: Subtitle
- Simulating Large Eliminations in Cedille
- Creators
- Christopher JenkinsAndrew MarmadukeAaron Stump
- Resource Type
- Preprint
- Publication Details
- ArXiv.org
- DOI
- 10.48550/arxiv.2112.07817
- ISSN
- 2331-8422
- Language
- English
- Date posted
- 12/14/2021
- Academic Unit
- Computer Science
- Record Identifier
- 9984411090102771
Metrics
4 Record Views