🔭 First-Class Telescopes

[TOTBWF]

Patch Description

This PR adds a first-class notion of telescope, and unifies

Motivation

Right now, we have some Cool tricks for records; namely record patches [#274] and total space conversion [#280]. However, these are somewhat ad-hoc tricks that are implemented entirely in the evaluator, and as such are somewhat clumsy. Furthermore, the recent work on first-class inductives [#299] has recently run into a snag: We don't have a good way of bundling up the methods of induction! Further on the horizon, the module system looms, with it's myriad of tricky features.

All of this points to one thing; we need some way of talking about telescopes from within the theory. Let's explore each of these problems deeper to see why.

Records

Right now, our records are nicer, slightly more efficient iterated sigma types. This is fine, but it makes some of the Cool Ideas a bit janky to implement. One only has to look at https://github.com/RedPRL/cooltt/blob/main/src/core/Refiner.ml#L701 to see how ugly things can get! It also is somewhat unclear how principled some of these operations are: they feel more like wacky macros that have been stapled onto the theory instead of operations that have types + semantics. To give these things types and make them honest-to-god operations, we need a way of talking about the binding structure of a sig type.

Inductive Types

Right now, the driving idea behind inductive types is that we can think about some declaration of an inductive as providing a context for an (extremely restricted) type theory. With this in mind, we can internalize this type theory into a language of descriptions, and then define an elimination principle by computing methods of induction for each of the descriptions in the datatype's context. However, we run into a snag when we try to bundle up all these methods of induction to create the method for the entire datatype. We want something like

method : (Γ : ctx) -> (a : desc) -> motive Γ -> tm Γ a -> type
methods : (Γ : ctx) -> motive Γ -> type
elim : (Γ : ctx) -> (p : motive Γ) -> methods Γ p -> (a : desc) -> (t : tm Γ a) -> method p t

but it's currently not clear how we bundle up those methods of induction, especially once we start considering HITs, whose ctx has telescopic structure. To get ourselves out of this jam, we need some way to talk about telescopic structure.

Modules

This is the least immediate of the 3 issues, but the most exciting. Our current vision is to make modules + records one and the same; however, a usable module system requires quite a few operations that our current system would struggle to support. In no particular order, these are:

• include, which adds all of the bindings from another module into the current one.
• Agda-style parameterized modules

We could implement these in a similar fashion to patches/total space conversion, but again this seems unprincipled. Furthermore, as we come up with new ideas, we have to keep adding elaborator hacks! Therefore, it seems much more elegant to have first-class notion of telescope so all of these hacks become actual, well-typed operations.

Design

The basic idea is to add the following datatypes to the core (examples written in Agda for clarity):

data Symbol = ...

data Telescope : Set where
   []  : Telescope
   _∷_ : Symbol → (A : Set) → (A → Telescope) → Telescope

The idea here is that Symbol represents a "quoted identifier", and telescope encodes the binding structure of, well, a telescope. We don't add an eliminator for Symbol, only for Telescope.

Then, we replace the list of types in sig with a term of type telescope. With this single change, we can give all of our previous hacks types, and make them operations that compute 🙂

There is one subtlety around Symbol. In order to make the elimination form for telescope sensible, we need to have these quoted identifiers. Otherwise, if we try to eliminate a telescope into the type telescope, we lose all of our names and get owned. However, changing everything over to using these quoted symbols makes things muuuuch more complicated.

The solution is to use the same "virtual type" machinery as the interval/cofibrations. By stratifying the theory, we make it safe to unquote these things all over the place, as we know that we won't ever get into a situation where we have an cut of type symbol when we need to extract out the identifier (for instance, when performing a projection).