TL;DR
This paper introduces a method within Cedille type theory to derive efficient Mendler-style lambda-encoded inductive datatypes with an induction principle and constant-time destructor, enabling space-efficient natural numbers.
Contribution
It relaxes functoriality constraints in lambda encodings and provides a generic approach to derive induction and constant-time destructors in Cedille.
Findings
Derived induction principle for Mendler-style lambda-encoded datatypes
Implemented constant-time destructor for lambda-encodings
Defined space-efficient lambda-encoded natural numbers
Abstract
It is common to model inductive datatypes as least fixed points of functors. We show that within the Cedille type theory we can relax functoriality constraints and generically derive an induction principle for Mendler-style lambda-encoded inductive datatypes, which arise as least fixed points of covariant schemes where the morphism lifting is defined only on identities. Additionally, we implement a destructor for these lambda-encodings that runs in constant-time. As a result, we can define lambda-encoded natural numbers with an induction principle and a constant-time predecessor function so that the normal form of a numeral requires only linear space. The paper also includes several more advanced examples.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
