# First-class functors

**Yufei Cai**

ResearcherYufei Cai, **Paolo Giarrusso**

ResearcherPaolo G. Giarrusso, **Klaus Ostermann**

HeadKlaus Ostermann

### Introduction

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-**C**lass **Reg**ular 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.

**Abstract:** Traversing an algebraic datatype by hand requires boilerplate
code which duplicates the structure of the datatype.
Datatype-generic programming (DGP) aims to eliminate such
boilerplate code by decomposing algebraic datatypes into type
constructor applications from which generic traversals can be
synthesized. However, different traversals require different
decompositions, which yield isomorphic but unequal types. This
hinders the interoperability of different DGP techniques.

In this paper, we propose Fωμ, an extension of the higher-order polymorphic lambda calculus Fω with records, variants, and equirecursive types. We prove the soundness of the type system, and show that type checking for first-order recursive types is decidable with a practical type checking algorithm. In our soundness proof we define type equality by interpreting types as infinitary λ-terms (in particular, Berarducci-trees). To decide type equality we β-normalize types, and then use an extension of equivalence checking for usual equirecursive types.

Thanks to equirecursive types, new decompositions for a datatype can be added modularly and still interoperate with each other, allowing multiple DGP techniques to work together. We sketch how generic traversals can be synthesized, and apply these components to some examples.

Since the set of datatype decomposition becomes extensible, System Fωμ enables using DGP techniques incrementally, instead of planning for them upfront or doing invasive refactoring.

# News

## Presentation at POPL symposium

**Yufei Cai**

ResearcherYufei Cai presents the paper *System F _{ω}
with Equirecursive Types for Datatype-generic Programming* at the
Symposium on Principles of Programming Languages in
St. Petersburg, Florida. The paper is joint work with

**Paolo Giarrusso**

ResearcherPaolo Giarrusso and

**Klaus Ostermann**

HeadKlaus Ostermann.

Read more ...

## Preprint for POPL paper online

The preprint for our paper on equirecursive types in System Fω, with title
“System Fω with Equirecursive Types for Datatype-generic Programming”, is now
available online.

Read more ...

## Paper accepted at POPL

Our paper on equirecursive types in System Fω, with title “System Fω
with Equirecursive Types for Datatype-generic Programming”, has been
accepted for presentation at the annual Symposium on Principles of
Programming Languages.

Read more ...

## Talk at Paris Diderot about functors

**Yufei Cai**

ResearcherYufei Cai gives an informal talk about the ongoing first-class
functors project at PPS Lab, University Paris
Diderot.

Read more ...