Showing cs.PLShow all
2 papers · 1 filter
cs.PL2018
Efficient Mendler-Style Lambda-Encodings in Cedille
Denis Firsov, Richard Blair, Aaron Stump
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 deri…
cs.PL2018
Generic Zero-Cost Reuse for Dependent Types
Larry Diehl, Denis Firsov, Aaron Stump
Dependently typed languages are well known for having a problem with code reuse. Traditional non-indexed algebraic datatypes (e.g. lists) appear alongside a plethora of indexed var…