-
DeLaM: A Dependent Layered Modal Type Theory for Meta-programming
Authors:
Jason Z. S. Hu,
Brigitte Pientka
Abstract:
We scale layered modal type theory to dependent types, introducing DeLaM, dependent layered modal type theory. This type theory is novel in that we have one uniform type theory in which we can not only compose and execute code, but also intensionally analyze the code of types and terms. The latter in particular allows us to write tactics as meta-programs and use regular libraries when writing tact…
▽ More
We scale layered modal type theory to dependent types, introducing DeLaM, dependent layered modal type theory. This type theory is novel in that we have one uniform type theory in which we can not only compose and execute code, but also intensionally analyze the code of types and terms. The latter in particular allows us to write tactics as meta-programs and use regular libraries when writing tactics. DeLaM provides a sound foundation for proof assistants to support type-safe tactic mechanism.
△ Less
Submitted 25 April, 2024;
originally announced April 2024.
-
Layered Modal Type Theories
Authors:
Jason Z. S. Hu,
Brigitte Pientka
Abstract:
We introduce layers to modal type theories, which subsequently enables type theories for pattern matching on code in meta-programming and clean and straightforward semantics.
We introduce layers to modal type theories, which subsequently enables type theories for pattern matching on code in meta-programming and clean and straightforward semantics.
△ Less
Submitted 28 February, 2024; v1 submitted 10 May, 2023;
originally announced May 2023.
-
A Categorical Normalization Proof for the Modal Lambda-Calculus
Authors:
Jason Z. S. Hu,
Brigitte Pientka
Abstract:
We investigate a simply typed modal $λ$-calculus, $λ^{\to\square}$, due to Pfenning, Wong and Davies, where we define a well-typed term with respect to a context stack that captures the possible world semantics in a syntactic way. It provides logical foundation for multi-staged meta-programming. Our main contribution in this paper is a normalization by evaluation (NbE) algorithm for…
▽ More
We investigate a simply typed modal $λ$-calculus, $λ^{\to\square}$, due to Pfenning, Wong and Davies, where we define a well-typed term with respect to a context stack that captures the possible world semantics in a syntactic way. It provides logical foundation for multi-staged meta-programming. Our main contribution in this paper is a normalization by evaluation (NbE) algorithm for $λ^{\to\square}$ which we prove sound and complete. The NbE algorithm is a moderate extension to the standard presheaf model of simply typed $λ$-calculus. However, central to the model construction and the NbE algorithm is the observation of Kripke-style substitutions on context stacks which brings together two previously separate concepts, structural modal transformations on context stacks and substitutions for individual assumptions. Moreover, Kripke-style substitutions allow us to give a formulation for contextual types, which can represent open code in a meta-programming setting. Our work lays the foundation for extending the logical foundation by Pfenning, Wong, and Davies towards building a practical, dependently typed foundation for meta-programming.
△ Less
Submitted 20 February, 2023; v1 submitted 22 November, 2022;
originally announced November 2022.
-
An Investigation of Kripke-style Modal Type Theories
Authors:
Jason Z. S. Hu,
Brigitte Pientka
Abstract:
This technical report investigates Kripke-style modal type theories, both simply typed and dependently typed. We examine basic meta-theories of the type theories, develop their substitution calculi, and give normalization by evaluation algorithms.
This technical report investigates Kripke-style modal type theories, both simply typed and dependently typed. We examine basic meta-theories of the type theories, develop their substitution calculi, and give normalization by evaluation algorithms.
△ Less
Submitted 10 May, 2023; v1 submitted 15 June, 2022;
originally announced June 2022.
-
A Category Theoretic View of Contextual Types: from Simple Types to Dependent Types
Authors:
Jason Z. S. Hu,
Brigitte Pientka,
Ulrich Schöpp
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 stand…
▽ More
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..
△ Less
Submitted 7 June, 2022; v1 submitted 6 June, 2022;
originally announced June 2022.
-
Internal Category with Families in Presheaves
Authors:
Jason Z. S. Hu
Abstract:
In this note, we review a construction of category with families (CwF) in a presheaf category. When the base category of a presheaf category is a CwF, we internalize this CwF structure in the CwF of the presheaf category. This note assumes working knowledge on category theory.
In this note, we review a construction of category with families (CwF) in a presheaf category. When the base category of a presheaf category is a CwF, we internalize this CwF structure in the CwF of the presheaf category. This note assumes working knowledge on category theory.
△ Less
Submitted 2 March, 2021;
originally announced March 2021.
-
Formalizing of Category Theory in Agda
Authors:
Jason Z. S. Hu,
Jacques Carette
Abstract:
The generality and pervasiness of category theory in modern mathematics makes it a frequent and useful target of formalization. It is however quite challenging to formalize, for a variety of reasons. Agda currently (i.e. in 2020) does not have a standard, working formalization of category theory. We document our work on solving this dilemma. The formalization revealed a number of potential design…
▽ More
The generality and pervasiness of category theory in modern mathematics makes it a frequent and useful target of formalization. It is however quite challenging to formalize, for a variety of reasons. Agda currently (i.e. in 2020) does not have a standard, working formalization of category theory. We document our work on solving this dilemma. The formalization revealed a number of potential design choices, and we present, motivate and explain the ones we picked. In particular, we find that alternative definitions or alternative proofs from those found in standard textbooks can be advantageous, as well as "fit" Agda's type theory more smoothly. Some definitions regarded as equivalent in standard textbooks turn out to make different "universe level" assumptions, with some being more polymorphic than others. We also pay close attention to engineering issues so that the library integrates well with Agda's own standard library, as well as being compatible with as many of supported type theories in Agda as possible.
△ Less
Submitted 6 January, 2021; v1 submitted 14 May, 2020;
originally announced May 2020.
