The n-Category Café

I’m aware of the folks working on general initiality theorems; in fact I mentioned them specifically in the post:

Others… are… attempting to give a general definition of “type theory” and prove a general initiality theorem for all such “type theories”.

as well as the relationship between this project and theirs:

I don’t view such a project as a replacement for proving one general theorem, but as a complementary effort, whose goals are primarily understanding and exposition.

I’ve also already spoken to Peter Lumsdaine and Andrej Bauer about this project, and both agreed that it seemed complementary to their effort and worth pursuing at the same time.

And also, to be frank, I don’t want to wait any longer. I think it’s gotten to the point that even someone who doesn’t believe it’s intrinsically important to write down initiality theorems completely might still agree that the existence of the controversy, and its failure to get resolved in a timely manner, is damaging enough to the perception of our subject among other mathematicians to make it worth the effort.

Personally, I also have another motivation: I want to understand the proofs of initiality theorems, and the best way to understand a proof is to help create it yourself. And I hope that everyone else who joins in this project will derive the same benefit of increased understanding.

I thought of something like that. But my impression is that Polymath projects have mainly been trying to solve important open problems by collecting lots of ideas from many contributors, and I wouldn’t put initiality theorems at that level. In particular, I wouldn’t want to give other mathematicians the impression that type theory and HoTT have nothing better to offer as a Polymath project than what is, essentially, a big bookkeeping problem.

Obviously this is closely related to my own opinion about the status and importance of initiality, which I tried to shy away from stating outright in the main announcement. The participants in this project don’t, after all, have to agree on the status and importance of initiality; all we need is the common goal of writing down a proof of it.

Mike started an nLab page on bidirectional typechecking a few days ago.

This is a really interesting question, and one that I’ve thought about a lot as well.

If we take the Streicher approach of first defining a partial interpretation function on raw judgments of the form $\Gamma \vdash M : A$, and then proving by induction on derivations that it is total on derivable judgments, then I don’t know how to get away from annotations even in a bidirectional theory. For instance, in an un-annotated application $App(F,X)$, where $F$ could be some arbitrary term, there is no way to produce from the raw syntax judgments of the form $\Gamma \vdash F : ?$ and $\Gamma \vdash X : ?$ that we could interpret inductively in order to apply the one to the other. These judgments only come from a bidirectional derivation of $\Gamma \vdash App(F,X) \Leftarrow C$ which first synthesizes a type $\Pi(x:A) B[x]$ for $F$ and then checks $X$ at type $A$. Unless there is some trick that I’m missing?

However, with a bidirectional system it becomes much more tempting to take a different approach than Streicher’s and define the interpretation function directly on derivations rather than bothering about a partial interpretation on raw judgments. Last year I proposed doing this with a bidirectional system of the “hereditary substitution” variety, in which only normal/canonical (and neutral/atomic) terms exist, in the hopes that it would have more direct higher-categorical semantics. At the time there didn’t seem to be much interest, but I still like that idea.

But even if we didn’t go all the way to hereditary substitution and used a bidirectional theory that does include non-normal terms (e.g. with type ascriptions to make redexes typable), we could still consider defining an interpretation by induction on derivations rather than raw judgments. As I understand it, the problem with doing this for a unidirectional theory (is that the opposite of “bidirectional”?) is that the conversion rule

$$\frac{\Gamma \vdash M:A \quad \Gamma\vdash A\equiv B\; type}{\Gamma\vdash M:B}$$

means that one derivable judgment has many different derivations, whereas we eventually want an interpretation function that depends only on the judgment and not how it was derived. But a bidirectional theory eliminates (or at least reduces) this ambiguity by pushing all uses of the conversion rule into canonical places (the switch between checking and synthesizing mode), so that every derivable judgment has a canonical (or maybe even unique?) derivation.

However, right now my inclination is that it would be better for this project to start out using the “traditional” Streicherian approach for a unidirectional theory with unpleasant annotations, and regard a bidirectional theory as “syntactic sugar” that can be “compiled” into the fully annotated theory before being interpreted, as Andy and Peter suggested below. (I believe this “compilation” idea has already been made fully precise for some type theories in the literature, by enhancing the bidirectional typing judgments to include a fully annotated “output” term that gets produced as you go along.)

I don’t know whether I agree with Peter that this will be cleaner. In fact, I quite like the idea that with a bidirectional theory we might be able to do away with the partial interpretation function and induct directly on derivations (and potentially also induct directly into higher categories without needing to strictify them). But the only way to really find out which approach is cleaner is to actually do both of them, and it makes sense to start with the one that’s already better-understood.

Furthermore, bidirectional typechecking is an extra layer of complication in the presentation of a type theory, and since a primary goal of this project is expositional, we want the result to be as accessible as possible to as many readers as possible. For instance, it would be nice if someone whose main exposure to type theory has been the HoTT book (including the brief appendix about formal syntax) could dive right into reading this initiality proof, and for that purpose it would be best to stick as close as possible to easier-to-understand unidirectional theories.

I think my response to Paolo is the same. Going through a calculus with explicit substitutions is an interesting idea, but in order to tell whether it’s better we have to actually do both versions, and to start with I would rather keep the type theory as close as possible to the ones that we use in practice, with implicit substitutions.

This is all just my current opinion, though. I’m coordinating the project (because someone has to), but I’m not the dictator, and I can be convinced or overruled.

For the $1,\Sigma, \Pi$ fragment of type theory, using a bidirectional framework ought to be something you can make work. It even seems likely you could get as far as a canonical forms presentation which omits definitional equality. (This would let you easily show that derivations and typed terms are in 1-1 correspondence.)

However, once you add positive types, things get more complicated, and AFAICT universes make this approach incredibly hairy. Basically once you have type variables you have to mark neutral terms of variable type to eta-expand them on-demand. (I learned this from Aleks Nanevski and company’s 2006 paper “Hoare Type Theory, Polymorphism and Separation”. It’s a nice idea, but one I’ve never seen much follow up to.)

As far as the issue of explicit substitutions or not goes, I think it hinges on the choice of de Bruijn notation or not. If you use de Bruijn notation then you will need explicit weakening markers in your syntax, from which explicit substitutions are not a big step. If you have explicit variable names you can omit the weakenings in the term syntax (because weakening maps between contexts with names are unique).

I don’t know whether de-Bruijn+explicit-substitution or named+no-substitutions is easier, but those two seem like the two most reasonable choices to me.

Actually, though, now that I think about it more, it seems that some amount of bidirectionality is already lurking in the ‘standard’ approach to initiality, and making it explicit might be helpful. For instance, in Peter’s sketch he wrote

For each (e : Expr cl γ), where cl is a syntactic class and γ a context-of-variables, we’ll give:

• in case cl=ty: for each X:C and partial environment for γ on X, a partial element of Ty X
• in case cl=tm: for each X:C and partial environment for γ on X, a partial element of Tm X

…

An alternative at this step: we could assume when interpreting terms that their type is already interpreted, i.e. define the goal type of the induction as

• in case cl=tm: for each X:C, partial environment for γ on X, and A in Ty Г, a partial element of (Tm X A)

This seems perhaps conceptually nicer than the version above, but that version seemed to work out slightly more easily in practice.

This seems to me to be essentially a semantic version of the difference between regarding $e$ as a synthesizing judgment or as a checking judgment. Even in a fully annotated theory where all terms can synthesize a type, there’s still room to distinguish the two judgments, because a term will synthesize only one syntactic type (at least, if the synthesis is single-valued functional), but should check against any type that is (judgmentally) equal to the type it synthesizes. And I suspect that if this sort of “mode switching” is not made explicit, it will nevertheless be implicitly embedded in the inductive clauses.

For instance, when interpreting an application $App^{x:A.B}(F,M)$, and (in Peter’s notation) an object $X:C$ and partial environment $E$, if we take the first approach (“all judgments are synthesizing”) we have to do something like:

• attempt to interpret $A$ over $(X,E)$, yielding $[[A]]:Ty(X)$
• attempt to interpret $B$ over $(X.[[A]], E.[[A]])$, yielding $[[B]]:Ty(X.[[A]])$
• attempt to interpret $F$ over $(X,E)$, yielding $[[F]]:Tm(X,P)$
• check that $P = \Pi [[A]] [[B]]$
• attempt to interpret $M$ over $(X,E)$, yielding $[[M]]:Tm(X,Q)$
• check that $Q = [[A]]$
• now the result is the semantic application of $[[F]]$ to $[[M]]$, in $Tm(X,[[M]]^*[[B]])$.

The paired steps of “interpret, yielding a (semantic) term in a (semantic) type, then check that the type equals something else” are exactly a semantic version of the mode-switching rule in a bidirectional theory:

$$\frac{\Gamma \vdash M \Rightarrow A \quad \Gamma \vdash A \equiv B}{\Gamma\vdash M \Leftarrow B}.$$

So even if we are not making any use of the ability of a bidirectional theory to omit annotations, it seems that it might still be helpful to distinguish synthesizing and checking judgments in the syntax, because they correspond to different modes of interpretation: when interpreting a synthesizing judgment we should produce a semantic term and its semantic type, while when interpreting a checking judgment we should take the semantic type as given and produce a semantic term belonging to it.

Additionally, if we set up the basic framework of the theorem using both judgments, then it will be more straightforward later to consider adding rules to the theory (or replacing existing ones) that make more use of bidirectionality.

I rather agree with Andy here: I’d expect it’ll be much cleaner to present initiality in terms of a fully annotated syntax, and leave the comparison with less-annotated syntax to be done entirely within the realm of syntax — much like how it is (I think) clearer to state initiality using a strict algebraic structure (CwA’s, contextual categories, …) and then give comparisons with weaker structures (type-theoretic fibration categories, …) purely in the categorical realm.

This disentangles the different things going on — proof-theoretic issues, initiality itself, and (higher-)category-theoretic issues.

I am not personally organizing a formalization aspect of the project at this time. However, it could be that other people would also be interested in a formalization, so if anyone else wanted to organize a parallel project to formalize the result of this one, you might get some takers.

Thanks for offering this! However, I think that for the current project we ought to stick to established ways of presenting type theories rather than experiment with new things: the point is to understand and exposit the state of the art.

Louis: The most important of them is the rule that reduces the instance of the induction rule for an inductive type A applied to its constructors into the identity function ‘λ(x:A).x’.

…

The possibility to reduce the “do nothing” inductive rules into the identity function should allow the definition of the classical type equivalence without identity types…

This sounds like eta reduction for inductive types. It’s known, but rarely used. I don’t understand how this could help express type equivalence.

For variable naming, I am using an index à la de Bruijn; however, the variable index I am using is defined as the position of the variable definition in the context (that is to say the size of the context where the variable is defined), so that a variable has a fixed index in a syntax expression.

In other words, you refer to a variable by it’s index from the left end of the context, rather than from the right end? So that when you bind a variable, and it appears on the right end, it doesn’t change the index of other variables? That’s de Bruijn “levels”. It’s distinguished from de Bruijn “indexes” because it has different properties.

(it is still possible to define some non universal “evil” properties - the HoTT identity types is one of them in the rule theory, where identity types match definitional equality)

It seems like you’re doing unusual things to avoid identity types. You seem to believe they will be “evil” in your setup. But in HoTT, identity types aren’t evil, they’re (homotopy-)invariant, like all type families. What’s up with this?

I would like to talk about your project, but perhaps this comments section is not an appropriate place to do so, if others agree (with Mike) that this initiality proof should not be trying something new and clever.

How about you re-announce on HoTT Cafe?