License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.TYPES.2021.9
URN: urn:nbn:de:0030-drops-167784
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2022/16778/
Jenkins, Christa ;
Marmaduke, Andrew ;
Stump, Aaron
Simulating Large Eliminations in Cedille
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 a broad family of datatype encodings. All results have been mechanically checked by Cedille, an implementation of CDLE.
BibTeX - Entry
@InProceedings{jenkins_et_al:LIPIcs.TYPES.2021.9,
author = {Jenkins, Christa and Marmaduke, Andrew and Stump, Aaron},
title = {{Simulating Large Eliminations in Cedille}},
booktitle = {27th International Conference on Types for Proofs and Programs (TYPES 2021)},
pages = {9:1--9:22},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-254-9},
ISSN = {1868-8969},
year = {2022},
volume = {239},
editor = {Basold, Henning and Cockx, Jesper and Ghilezan, Silvia},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2022/16778},
URN = {urn:nbn:de:0030-drops-167784},
doi = {10.4230/LIPIcs.TYPES.2021.9},
annote = {Keywords: large eliminations, generic programming, impredicative encodings, Cedille, Mendler algebra}
}
