Simulating Large Eliminations in Cedille

TL;DR

This paper demonstrates how to simulate large eliminations within the calculus of dependent lambda eliminations (CDLE), enabling expressive generic programming in a type theory that normally lacks this feature.

Contribution

It introduces a method to simulate large eliminations in CDLE, including a generic formulation and proof of correctness, validated by mechanical checking in Cedille.

Findings

Simulation of large eliminations is feasible within CDLE.

The approach is validated through case studies on various datatypes.

The method is mechanically verified 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 any datatype. All results have been mechanically checked by Cedille, an implementation of CDLE.