Functors are Type Refinement Systems

Functors are Type Refinement Systems
Paul-André Melliès and Noam Zeilberger
POPL 2015

The standard reading of type theory through the lens of category theory is based on the idea of viewing a type system as a category of well-typed terms. We propose a basic revision of this reading: rather than interpreting type systems as categories, we describe them as functors from a category of typing derivations to a category of underlying terms. Then, turning this around, we explain how in fact any functor gives rise to a generalized type system, with an abstract notion of typing judgment, typing derivations and typing rules. This leads to a purely categorical reformulation of various natural classes of type systems as natural classes of functors.

The main purpose of this paper is to describe the general framework (which can also be seen as providing a categorical analysis of refinement types), and to present a few applications. As a larger case study, we revisit Reynolds' paper on "The Meaning of Types" (2000), showing how the paper’s main results may be reconstructed along these lines.

This paper was quite a joy to read. The proposed framework feels simple yet penetrating, with convincing examples of elementary categorical constructions translating to non-trivial type system features. According to the second author, it is only the first in a series, with a much more advanced second one already available as a draft on the arXiv; I hope that this develops into a useful foundational setting for programming languages.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

I like it!

This is really, really neat!

Where's the algorithm?

Interesting question

Where's the algorithm?

That is an excellent question marco, thanks! Indeed, I wonder if this approach can shed new light on type inference questions; maybe existing results on fibrations or adjoint functors provide useful insight into the design and implementation of type inference engines.

Thumbs up.

Thanks for the link. I don't have anything useful to say, though.

Monoidal structure

I don't know if there's something to this, but the monoidal structure of refinements reminds me of the monoidal structure of nominal freshness in Schöpp and Stark's "A Dependent Type Theory with Names and Binding."