catlog/tt/mod.rs
1//! DoubleTT: type theory for models of a double category.
2//!
3//! This is developer documentation explaining how DoubleTT works "under the
4//! hood". It expects that you already know the basics of how to write models of
5//! double theories and morphisms between them using DoubleTT. A mathematical
6//! presentation of the type theory implemented here is available in the [math
7//! docs](https://next.catcolab.org/math/tt-0001.xml).
8//!
9//! To a first approximation, DoubleTT is a standard dependent type theory
10//! implemented using normalization by evaluation (following [Coquand's
11//! algorithm](https://doi.org/10.1016/0167-6423(95)00021-6)), so we start by
12//! explaining what that looks like.
13//!
14//! # Basics of normalization by evaluation (NbE)
15//!
16//! There are four data structures that form the core of this implementation, which
17//! may be arranged in a 2x2 grid:
18//!
19//! | | Syntax | Value |
20//! |------|--------|-------|
21//! | Term | [BaseTmS] | [BaseTmV] |
22//! | Type | [BaseTyS] | [BaseTyV] |
23//!
24//! Evaluation is the process of going from syntax to values. Evaluation is used to
25//! *normalize types*. We need to normalize types because there are many different
26//! syntaxes which may produces the same type. For instance, `b`, and `x.a` where
27//! `x : [ a : @sing b ]` are both the same type. Because types may depend on terms,
28//! we must also normalize terms. (Later we will see that we don't have to normalize
29//! *all* terms, but in a vanilla dependent type theory implementation, one does
30//! have to normalize all terms, and as we are reviewing the basics here, we will
31//! stick to that assumption).
32//!
33//! An evaluator for the untyped lambda calculus would look like the following code,
34//! which is in a "rust with a gc" syntax.
35//!
36//! ```ignore
37//! type BwdIdx = usize;
38//!
39//! enum BaseTmS {
40//! Var(BwdIdx),
41//! App(BaseTmS, BaseTmS),
42//! Lam(BaseTmS)
43//! }
44//!
45//! type Env = Bwd<Closure>;
46//!
47//! struct Closure {
48//! env: Env,
49//! body: BaseTmS
50//! }
51//!
52//! fn eval(env: Env, tm_s: BaseTmS) -> Closure {
53//! match tm_s {
54//! BaseTmS::Var(i) => env.lookup(i),
55//! BaseTmS::App(f, x) => {
56//! let fv = eval(env, f);
57//! let xv = eval(env, x);
58//! eval(fv.env.snoc(xv), fv.body)
59//! }
60//! BaseTmS::Lam(body) => Closure { env, body }
61//! }
62//! }
63//! ```
64//!
65//! This is a "closed" evaluator for lambda calculus, which means that a value is
66//! *always* a closure. What we need for type theory is an "open" evaluator,
67//! which means that a value is either a closure, or a variable. This permits us
68//! to normalize *past a binding*. For instance, we can normalize `λ x. (λ x. x) x`
69//! to `λ x. x`. This looks like the following:
70//!
71//! ```ignore
72//! type FwdIdx = usize;
73//!
74//! enum BaseTmV {
75//! // f a₁ ... aₙ
76//! Neu(FwdIdx, Bwd<BaseTmV>),
77//! Clo(Closure)
78//! }
79//!
80//! impl BaseTmV {
81//! fn app(self, arg: BaseTmV) -> BaseTmV {
82//! match self {
83//! BaseTmV::Neu(head, args) => BaseTmV::Neu(head, args.snoc(arg)),
84//! BaseTmV::Clo(clo) => eval(clo.env.snoc(arg), clo.body)
85//! }
86//! }
87//! }
88//!
89//! type Env = Bwd<BaseTmV>;
90//!
91//! fn eval(env: Env, tm_s: BaseTmS) -> Closure {
92//! match tm_s {
93//! BaseTmS::Var(i) => env.lookup(i),
94//! BaseTmS::App(f, x) => {
95//! let fv = eval(env, f);
96//! let xv = eval(env, x);
97//! fv.app(xv)
98//! }
99//! BaseTmS::Lam(body) => BaseTmV::Clo(Closure { env, body })
100//! }
101//! }
102//!
103//! fn quote(scope_len: usize, tm_v: BaseTmV) -> BaseTmS {
104//! match tm_v {
105//! BaseTmV::Neu(f, xs) =>
106//! xs.iter.fold(BaseTmS::Var(scope_len - f - 1), |f, x| BaseTmS::App(f, x)),
107//! BaseTmV::Clo(clo) => {
108//! let x_v = BaseTmV::Neu(scope_len, Bwd::Nil);
109//! let body_v = eval(clo.env.snoc(x_v), clo.body);
110//! BaseTmS::Lam(quote(scope_len + 1, body_v));
111//! }
112//! }
113//! }
114//! ```
115//!
116//! The normalization procedure is achieved by evaluating then quoting.
117//!
118//! In a way, evaluation is kind of like substitution, in that it replaces variables
119//! with values. However, the key difference is that evaluation creates closures
120//! that capture their environment, while substitution does not.
121//!
122//! # NbE in DoubleTT
123//!
124//! The implementation of NbE for DoubleTT is simplified compared to a generic
125//! dependent type theory because we need only normalize types for objects---and
126//! type dependency appears only for morphism types (which depend on a pair of
127//! objects). Therefore, we don’t need to worry about equality checking
128//! with respect to any morphism equalities which we might want to impose.
129//!
130//! # Specialization
131//!
132//! Another important feature of DoubleTT is *specialization*. We can see
133//! specialization at play in the following example. Let `Graph` and `Graph2` be
134//! the following double models.
135//!
136//! ```text
137//! model Graph := [
138//! E : Entity,
139//! V : Entity,
140//! src : (Id Entity)[E, V],
141//! tgt : (Id Entity)[E, V],
142//! ]
143//! /# declared: Graph
144//!
145//! model Graph2 := [
146//! V : Entity,
147//! g1 : Graph & [ .V := V ],
148//! g2 : Graph & [ .V := V ]
149//! ]
150//! /# declared: Graph2
151//! ```
152//!
153//! Then we can synthesize the type of `g.g1.V` in the context of a variable `g: Graph2`
154//! via:
155//!
156//! ```text
157//! syn [g: Graph2] g.g1.V
158//! /# result: g.g1.V : @sing g.V
159//! ```
160//!
161//! We can also normalize `g.g1.V` in the context of a variable `g: Graph2`:
162//!
163//! ```text
164//! norm [g: Graph2] g.g1.V
165//! /# result: g.V
166//! ```
167//!
168//! This shows how the specialization `g1 : Graph & [ .V := V ]` influences the type
169//! and normalization of the `.g1.V` field of a model of `Graph2`.
170//!
171//! Specialization is a way of creating *subtypes* of a record type by setting the
172//! type of a field to be a subtype of its original type. So in order to understand
173//! specialization, one must first understand subtyping. In DoubleTT, there are
174//! two ways to form subtypes. We write `A <: B` for "`A` is a subtype of `B`".
175//!
176//! 1. If `a : A`, then `@sing a <: A`.
177//! 2. If `A` is a record type with a field `.x`, and `B` is a subtype of the type of
178//! `a.x` for a generic element `a : A`, then `A & [ .x : B ] <: A`. The notation `A
179//! & [ .x := y ]` is just syntactic sugar for `A & [ .x : @sing y ]`.
180//!
181//! Crucially, the type of `a.x` may depend on the values of other fields of `a`, so
182//! it is important that the subtyping check is performed in the context of a *generic*
183//! element of `A`. In the above case, the type of `g1.V` is `Entity` for a generic
184//! `g1 : Graph`, and as `V : Entity`, we have `@sing V <: Entity` as required for
185//! `Graph & [ .V := V ]` to be a well-formed type.
186//!
187//! Note that some algorithms simply ignore specializations, for instance
188//! [`eval::Evaluator::convertible_ty`]. This is convenient, because it means
189//! that checking whether two types are subtypes can be reduced to checking
190//! whether they are convertible, and then checking whether a generic element of
191//! the first type is an element of the second type. This neatly resolves the
192//! difference between `[ x : @sing a ]` and `[ x : Entity ] & [ .x := a ]`,
193//! which are represented differently, but should be semantically the same type.
194
195pub mod batch;
196pub mod context;
197pub mod eval;
198pub(in crate::tt) mod fiber_elab;
199pub mod modelgen;
200pub mod notebook_elab;
201pub mod prelude;
202pub mod stx;
203pub mod text_elab;
204pub mod theory;
205pub mod toplevel;
206pub mod val;
207pub mod wd;
208
209#[cfg(doc)]
210use stx::*;
211#[cfg(doc)]
212use val::*;