Higher-order containers

Abstract

Containers are a semantic way to talk about strictly positive types. In previous work it was shown that containers are closed under various constructions including products, coproducts, initial algebras and terminal coalgebras. In the present paper we show that, surprisingly, the category of containers is cartesian closed, giving rise to a full cartesian closed subcategory of endofunctors. The result has interesting applications in generic programming and representation of higher order abstract syntax. We also show that the category of containers has finite limits, but it is not locally cartesian closed. © 2010 Springer-Verlag Berlin Heidelberg.