This is the homepage of the first-class functors project. Our goal is to support as many datatype-related functors as first-class objects as possible, as conveniently as possible. So far we managed to practically support regular functors and demonstrate type-soundness in the presence of higher-kinded functors.
The source code of a prototype library for first-class regular functors is available for free under the MIT license:
CREG: First-Class Regular Functors.
Email us questions.
Here are some slides of a talk at IFIP
WG2.11 (Jan. 2015) by Klaus Ostermann
Paper (POPL 2016): System F-omega with Equirecursive Types for Datatype-generic Programming
Technical report version with full proofs.
Slides of paper presentation.
Participating Team Members
System F-Omega with Equirecursive Types for Datatype-Generic Programming
by Yufei Cai, Paolo G. Giarrusso, and Klaus Ostermann
In Proceedings of Symposium on Principles of Programming Languages (POPL 2016), pages 30–43, 2016.Learn More