Higher-Order Containers

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 applicageneric programming and representation of higher order abstract syntax. We also show that while the category of containers has finite limits, it is not locally cartesian closed.

• Type: Conference
• Year: 2010
• Where: CIE
• Authors: Thorsten Altenkirch, Paul Levy, Sam Staton
• Keywords: Applied Computing, Cartesian Closed, Cartesian Closed Subcategory, CIE 2010, Containers