You find yourself, like Jacob, gazing up the rungs (for me, ropes)
of a ladder that seems to have constructed itself
to avoid leaving you flat on the ground.
But what, you ask, in the arching presence of the angels,
do you do at the top?
Type theories, to be consistent, cannot be uniform. Somewhere, your power must ebb, abstractions diminish, until finally you are left with the beautiful silence of a single symbol (maybe ). Type : type is also beautiful, but long known to be inconsistent: collapsing everything to one level ruins your type theory as a logic. There are more subtle examples of the need to give up your power as you ascend (this starts to sound like John of the Cross). You cannot repeat impredicative quantification one level up, for example: Girard proved this is paradoxical in his dissertation. So if you are an impredicativist as I am, your kind level must be strictly weaker than your type level.
But what about if you are a predicativist, perhaps a devotee (as I also am) of Agda? Agda, and also Coq via its ECC (Extended Calculus of Constructions, of Zhaohui Luo) structure, seem to avoid this quietist imperative I am mentioning. Above the current level, there is another, with essentially the same power. And beyond that, another, ad infinitum. The ladder goes up forever! We surpass the heavens!
But no, experienced Agda and Coq users know that is sadly not what happens. Much like the tower of Babel, the predicative universe hierarchy does not satisfy the desires of abstraction. For some constructions make sense at all levels, and hence we introduce the seductive ideas of typical ambiguity (considered for a system of Coquand’s which is a predecessor of ECC, by Harper and Pollack) and universe polymorphism (also considered by Harper and Pollack). Universe polymorphism as I understood it from Agda seems a bit different from what Harper and Pollack propose. And it seems that typical ambiguity is found more in Coq than Agda. (I could be wrong on these points!) In Agda, there seems to be the curious idea that we can quantify over all levels of the hierarchy explicitly. And we are then left with the conundrum of what level such a quantification itself has? Of course, for soundness reasons, it cannot have one of the levels covered by the level quantification. So we have to make up a new level, namely . And we see that level quantification was a charade to begin with: we are definitely not quantifying over all the levels, just some prefix of them. And it seems Agda does not make available to you to use in your code. So this just seems very hacky.
More principled is something that I think is closer to the kind of universe polymorphism that Harper and Pollack were proposing, which in their work is located at global definitions (not arbitrary terms). And this is the answer to my riddle at the beginning: when you reach the top of your ladder, you have to “go meta”. It is a beautiful insight that we can internalize the induction scheme one finds in Peano Arithmetic as a single second-order axiom. We have passed from the meta-level, with a family of formulas, to a single object-language formula. I propose that when we reach the top layer of our layered type theory, we do the reverse. We add schematic definitions.
Here at Iowa, we are working on this new Cedille type theory and system. Some of my recent papers are about this. There, we have a predicative hierarchy truncated at level 2. Ha! There are just terms, types, and kinds. It is actually more convenient to reach the end of the ladder faster! And going schematic means that while we do not support kind-level functions, we will allow you to define parametrized kinds. So you can give a top-level definition of some kind parametrized by terms or types. The definition itself does not need some funny type with level or some additional superkind structure. Of course, one can only use the definition with all parameters instantiated.
Simple, but extends expressivity a bit just out of the reach of what can be internalized in the theory.