A Category Theoretic View of Contextual Types: from Simple Types to Dependent Types

TL;DR

This paper provides a categorical semantics for Cocon, a contextual modal type theory, using presheaf models to unify simple and dependent types with a focus on syntax and invariants.

Contribution

It introduces a presheaf-based categorical model for Cocon, capturing contextual objects and extending to dependent types within a unified semantic framework.

Findings

Presheaf models effectively characterize Cocon's contextual objects.

A comonad $lat$ models closed elements, capturing substitution invariance.

Fragment of Cocon modeled without recursor in Fitch-style dependent modal type theory.

Abstract

We describe the categorical semantics for a simply typed variant and a simplified dependently typed variant of Cocon, a contextual modal type theory where the box modality mediates between the weak function space that is used to represent higher-order abstract syntax (HOAS) trees and the strong function space that describes (recursive) computations about them. What makes Cocon different from standard type theories is the presence of first-class contexts and contextual objects to describe syntax trees that are closed with respect to a given context of assumptions. Following M. Hofmann's work, we use a presheaf model to characterise HOAS trees. Surprisingly, this model already provides the necessary structure to also model Cocon. In particular, we can capture the contextual objects of Cocon using a comonad $\flat$ that restricts presheaves to their closed elements. This gives a simple semantic characterisation of the invariants of contextual types (e.g. substitution invariance) and identifies Cocon as a type-theoretic syntax of presheaf models. We further extend this characterisation to dependent types using categories with families and show that we can model a fragment of Cocon without recursor in the Fitch-style dependent modal type theory presented by Birkedal et. al..