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

DOI10.1145/3545115MaRDI QIDQ5056372zbMATH OpenOpenAlexFDO

Authors Jason Z. S. Hu, Brigitte Pientka, Ulrich Schöpp

Publication date 8 December 2022

Published in ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2206.02831

zbMATH Keywords

category theorycontextual typesdependent typestype theory

Mathematics Subject Classification ID

Type theory (03B38) Combinatory logic and lambda calculus (03B40) Modal logic (including the logic of norms) (03B45) Presheaves and sheaves, stacks, descent conditions (category-theoretic aspects) (18F20) Categories of fibrations, relations to (K)-theory, relations to type theory (18N45)

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..

Recommendations

• scientific article; zbMATH DE number 4187810
• scientific article; zbMATH DE number 1241699
• Model structures on categories of models of type theories
• Internal type theory
• Revisiting the categorical interpretation of dependent type theory

Cites work

• A framework for defining logics
• A modal analysis of staged computation
• A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions
• Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description)
• Brouwer's fixed-point theorem in real-cohesive homotopy type theory
• Comprehension categories and the semantics of type dependency
• Contextual modal type theory
• Denotation of contextual modal type theory (CMTT): syntax and meta-programming
• Extending homotopy type theory with strict equality
• scientific article; zbMATH DE number 4049849 (Why is no real title available?)
• scientific article; zbMATH DE number 1241699 (Why is no real title available?)
• scientific article; zbMATH DE number 512773 (Why is no real title available?)
• scientific article; zbMATH DE number 7599980 (Why is no real title available?)
• Internal type theory
• Internal universes in models of homotopy type theory
• Modal dependent type theory and dependent right adjoints
• Semantical analysis of contextual types
• The biequivalence of locally Cartesian closed categories and Martin-Löf type theories
• Well-founded recursion over contextual objects

Cited in

(6)

• Semantical analysis of contextual types
• Combinatorial structure of type dependency
• scientific article; zbMATH DE number 6174931 (Why is no real title available?)
• Contextual types, explained. Invited tutorial
• ``Upon this quote I will build my Church thesis
• Semantics of pattern unification

Describes a project that uses

Uses Software

• MiniML

This page was built for publication: A Category Theoretic View of Contextual Types: From Simple Types to Dependent Types

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5056372)