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.

Source code

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.

Slides

Here are some slides of a talk at IFIP WG2.11 (Jan. 2015) by Klaus Ostermann
HeadKlaus 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

Yufei Cai

Paolo Giarrusso

Klaus Ostermann

Publications

News