nLab Initiality Project - Type Theory

Initiality Project - Type Theory

Initiality Project - Type Theory

This page is part of the Initiality Project.

Bidirectionality

All our terms are fully annotated. For instance, we write App (x:A)B(M,N)App^{(x:A)B}(M,N) rather than just App(M,N)App(M,N). It is, at best, unclear whether any less than fully annotated syntax can be used in an initiality theorem without “preprocessing” that is tantamount to annotating it.

In particular, this means that given Γ\Gamma and TT, if ΓT:A\Gamma \vdash T:A can be derived for any value of AA, then there is a canonical such AA that can be deduced syntactically, or synthesized, from Γ\Gamma and TT. For instance, if App (x:A)B(M,N)App^{(x:A)B}(M,N) has any type, then it must have the type B[N/x]B[N/x]. On the other hand, the conversion rule

ΓT:AΓABtypeΓT:B\frac{\Gamma \vdash T:A \qquad \Gamma \vdash A\equiv B \,type}{\Gamma \vdash T:B}

implies that App (x:A)B(M,N)App^{(x:A)B}(M,N) must also have any type that is judgmentally equal to B[N/x]B[N/x]. But although it has these types, there is a sense in which it “has” them in a different sense from the one unique one that it synthesizes. Moreover, the conversion rule is perhaps the ickiest thing to deal with in an initiality theorem, because it can be applied absolutely anywhere, over and over again, leading to many many different derivations of the same judgment that should not be distinguished semantically.

Note that since all our terms are fully annotated, all of our formation, introduction, and elimination rules can synthesize their types. However, the type annotations also tell us what types the subterms need to have (i.e. the types that must occur in the premises of the corresponding rule), in order for the term to have its canonical type. These types may not be syntactically equal to the types synthesized by the subterms, so we need to check subterms against the types we want. The check should succeed if and only if the subterm’s synthesized type is judgmentally equal to the one we want; and this is the only place that the conversion rule really needs to be applied. So in the App (x:A)B(M,N)App^{(x:A)B}(M,N) example, it synthesizes only B[N/x]B[N/x], up to syntactic equality, but it checks against any type judgmentally equal to B[N/x]B[N/x].

Type theorists have a standard technique for distinguishing these two situations and controlling the use of the conversion rule, known as bidirectional typechecking. Instead of one judgment ΓT:A\Gamma\vdash T:A, we have two typing judgments:

  • ΓTA\Gamma \vdash T \Rightarrow A: in context Γ\Gamma the term TT synthesizes the type AA. Here AA is, if it exists, uniquely determined by Γ\Gamma and TT: it is an “output” to their “inputs”.
  • ΓTA\Gamma \vdash T \Leftarrow A: in context Γ\Gamma the term TT checks against the type AA. Here Γ\Gamma, TT, and AA are all “inputs” and the only “output” is the truth value of whether the typecheck is valid.

Whereas unidirectional typing rules have the conversion rule, allowing the type to be changed at any point to a judgmentally equal one, with bidirectional typing rules, conversion is only used when switching from a synthesizing premise to a checking conclusion, using the “mode-switching” rule:

ΓTAΓABtypeΓTB\frac{\Gamma \vdash T\Rightarrow A \qquad \Gamma \vdash A\equiv B \,type}{\Gamma \vdash T\Leftarrow B}

Unlike typical versions of bidirectional typing, in our approach the checking judgment is defined solely by the mode-switching rule, and all other typing rules conclude a synthesizing judgment. This variant doesn’t help with typechecking algorithms, but it still factors out type conversion cleanly: the equality judgment is used when, and only when, the mode switches.

So in summary, terms formers are fully annotated, their typing rules synthesize a type in the conclusion, and have premises that check their subterms against appropriate types. So the mode-switching rule gets applied a lot, because it’s the only way, in our system, to derive a checking judgment.

From a syntactic perspective, there are many advantages of bidirectional typechecking, but it is unclear at present whether any of them are relevant to categorical semantics (although by using a bidirectional framework we are better placed to take advantage of them if they do become relevant). But more importantly, the natural structure of the semantic interpretation, as suggested by Peter Lumsdaine, matches the syntactic bidirectional picture quite closely, and it may be clarifying to make that analogy more precise.

Typical versions of bidirectional typing also have bidirectional equality rules, which essentially implement an algorithm for equality-checking. (Such partially-type-directed algorithms have advantages over simply normalizing both terms and comparing normal forms, such as more easily incorporating eta-conversion.) However, since we want our theorem to generalize to type theories in which equality is not algorithmic (e.g. theories with equality reflection) — and more importantly, since in semantic equality there is no “output information” to ever compute — we will not orient our equality judgments.

Our sort of bidirectional theory is very closely related to a unidirectional theory that may be more familiar to some readers. Roughly speaking, to go from a unidirectional theory to our sort of bidirectional one: make sure everything is fully annotated, make the conclusions of formation/introduction/elimination rules synthesizing and their premises checking, and replace the conversion rule by the mode-switching rule. Oppositely, to recover a unidirectional theory from our bidirectional one, simply collapse both checking and synthesizing judgments into the “term has a type” judgment T:AT:A, thereby generalizing the mode-switching rule to the conversion rule. Below we will make this “isomorphism” a bit more precise.

Contexts

A raw context is a finite list of pairs consisting of a variable and a raw term in which the variables occurring are all pairwise distinct. Each such pair, written x:Ax:A, is called a typing declaration, with AA being a type to which the variable xx belongs.

A valid context is a raw context (x 1:A 1,,x n:A n)(x_1:A_1, \dots ,x_n:A_n) such that each judgment x 1:A 1,,x k:A kA k+1typex_1:A_1,\dots, x_k:A_k \vdash A_{k+1} \, type is derivable by the rules below. This notion is defined a posteriori after the primitive rules for all the judgments have been given. In particular, the judgments themselves never refer to context validity. The intuitive interpretation of a judgment-in-context Γ𝒥\Gamma\vdash \mathcal{J} should therefore be “if Γ\Gamma is a valid context, then 𝒥\mathcal{J} holds in that context” (and this is the meaning we will give it semantically).

Judgment forms

Our type theory has five judgment forms. Here Γ\Gamma is a metavariable ranging over raw contexts, while S,T,A,BS,T,A,B are metavariables ranging over raw terms.

  1. ΓAtype\Gamma \vdash A\,type — “AA is a type in context Γ\Gamma”.
  2. ΓTA\Gamma \vdash T \Leftarrow A — “TT can be checked to have type AA in context Γ\Gamma
  3. ΓTA\Gamma \vdash T \Rightarrow A — “TT synthesizes the type AA in context Γ\Gamma
  4. ΓABtype\Gamma \vdash A \equiv B \, type — “AA and BB are judgmentally equal types in context Γ\Gamma
  5. ΓST:A\Gamma \vdash S \equiv T : A — “SS and TT are judgmentally equal terms of type AA in context Γ\Gamma

Modes, preconditions, etc.

All the metavariables occurring in all of our judgments should be regarded as “inputs”, with the sole exception that AA in the synthesizing judgment ΓTA\Gamma \vdash T \Rightarrow A is an output. In other words, if we regard “searching for a derivation of some judgment” as an “algorithm”, with the rules for deriving that judgment as the “cases to try” and their premises as the resulting “recursive calls”, then in all but one case the algorithm takes all the arguments of the judgment as inputs and returns only a truth value, while in the exceptional case ΓTA\Gamma \vdash T \Rightarrow A it takes Γ\Gamma and TT as inputs and returns AA as output (if it succeeds, otherwise it returns failure).

Note, though, that because our judgmental equality is not bidirectional and need not be even semidecidable, these “algorithms” are not really algorithms, unless we regard the equality judgment as a sort of “oracle” that they can invoke.

Similarly, we regard validity of all the “inputs” of each judgment as something that the “caller” should ensure, while validity of the “output” as something that the function returning it should “promise”. For example, the rules for deriving a judgment such as ΓTA\Gamma \vdash T \Leftarrow A need only be “correct” under the assumption that Γ\Gamma is a valid context and ΓAtype\Gamma \vdash A\,type, but in turn these assumptions must ensure that all the analogous “preconditions” of all premises of such rules hold.

Primitive rules

Structural rules

The main structural rule is the “variable” or “hypothesis” rule, which says that if a variable is declared in a context, then as a term it synthesizes the type that it is declared with:

(x:A)ΓΓxA \frac{(x:A) \in \Gamma}{\Gamma \vdash x \Rightarrow A}

The other structural rules of weakening, contraction, and substitution will be admissible.

Mode-switching rule

The mode-switching rule says that to check that a term has a given type, we first synthesize a type for that term and then check that this type equals the given one. In our fully annotated system, this is the only way to derive the checking judgment ΓTB\Gamma \vdash T \Leftarrow B.

ΓTAΓABtypeΓTB \frac{\Gamma \vdash T \Rightarrow A \qquad \Gamma \vdash A \equiv B \, type}{\Gamma \vdash T \Leftarrow B}

This is also the only incarnation of the conversion rule, which in a “unidirectional” system is

ΓT:AΓABtypeΓT:B. \frac{\Gamma \vdash T : A \qquad \Gamma \vdash A \equiv B \, type}{\Gamma \vdash T : B.}

A bidirectional system controls this rule more carefully, enforcing it to be used (when and) only when the mode switches.

Equality rules

We have primitive rules asserting that equality of terms and types are both reflexive, transitive, and symmetric, and moreover that equality of terms is invariant under equality of types.

For equality of types ΓAB\Gamma \vdash A \equiv B, we take as input that ΓAtype\Gamma \vdash A\,type and ΓBtype\Gamma \vdash B\,type, so we don’t need any premise in the reflexivity rule, but we do need one in the transitivity rule.

ΓAAtype\frac{}{\Gamma \vdash A \equiv A type}
\,
ΓABtypeΓBAtype\frac{\Gamma \vdash A \equiv B type}{\Gamma \vdash B \equiv A type}
\,
ΓBtypeΓABtypeΓBCtypeΓACtype\frac{\Gamma \vdash B\,type\qquad \Gamma\vdash A \equiv B type \qquad \Gamma\vdash B \equiv C type}{\Gamma \vdash A \equiv C type}

Similarly ΓTS:A\Gamma \vdash T \equiv S : A takes as input that ΓTA\Gamma \vdash T \Leftarrow A and ΓSA\Gamma \vdash S \Leftarrow A. It also takes ΓAtype\Gamma \vdash A type.

ΓTT:A\frac{ }{\Gamma \vdash T \equiv T : A}
\,
ΓTS:AΓST:A\frac{\Gamma \vdash T \equiv S : A}{\Gamma \vdash S \equiv T : A}
\,
ΓSAΓTS:AΓSR:AΓTR:A\frac{\Gamma \vdash S \Leftarrow A \qquad \Gamma \vdash T \equiv S : A\qquad \Gamma \vdash S \equiv R : A}{\Gamma \vdash T \equiv R : A}
\,
ΓAtypeΓTS:AΓABtypeΓTS:B\frac{\Gamma \vdash A\,type \qquad \Gamma \vdash T \equiv S : A \qquad \Gamma \vdash A \equiv B type}{\Gamma \vdash T \equiv S : B}

Constant rules

TODO. In fact, specifying the constant rules is part of the “signature”.

Type former rules

Each type former (Π\Pi-types, Σ\Sigma-types, etc.) has a collection of rules giving its

  • formation rule (when is it a valid type)
  • introduction rule (what terms synthesize this type)
  • elimination rule (how terms in this type can be used)
  • equality rules (beta-reduction and, sometimes, eta-conversion)
  • congruence rules (the type former and its introduction and elimination forms respect judgmental equality)

Π\Pi-types

ΓAtypeΓ,x:ABtypeΓΠ(x:A).Btype ΓAtypeΓ,x:ABtypeΓMΠ(x:A).BΓNAΓApp x:A.B(M,N)B[N/x] ΓAtypeΓ,x:ABtypeΓ,x:AMBΓλ(x:A.B).MΠ(x:A).B ΓAAtypeΓ,x:ABBtypeΓApp x:A.B(λ(x:A.B).M,N)M[N/x]:B[N/x] Γ,y:AApp x:A.B(M,y)App x:A.B(M,y):B[y/x]ΓMM:Π(x:A).B ΓAAtypeΓ,x:ABBtypeΓΠ(x:A)BΠ(x:A)Btype ΓAAtypeΓ,x:ABBtypeΓ,x:AMM:BΓλ(x:A.B).Mλ(x:A.B).M:Π(x:A).B ΓAAtypeΓ,x:ABBtypeΓMM:Π(x:A)BΓNN:AΓApp x:A.B(M,N)App x:A.B(M,N):B[N/x] \begin{gathered} \frac{\Gamma \vdash A \, type \qquad \Gamma, x:A \vdash B\,type}{\Gamma \vdash \Pi(x:A) .B \, type} \\ \\ \frac{\Gamma \vdash A \, type \qquad \Gamma, x:A \vdash B\,type \qquad \Gamma \vdash M \Leftarrow \Pi(x:A). B \qquad \Gamma \vdash N \Leftarrow A}{\Gamma \vdash App^{x:A.B}(M,N) \Rightarrow B[N/x]} \\ \\ \frac{\Gamma \vdash A \, type \qquad \Gamma,x:A \vdash B \,type \qquad \Gamma,x:A \vdash M \Leftarrow B}{\Gamma \vdash \lambda(x:A.B).M \Rightarrow \Pi(x:A). B} \\ \\ \frac{\Gamma\vdash A \equiv A' \, type \qquad \Gamma, x:A \vdash B \equiv B' \, type}{\Gamma \vdash App^{x:A.B}(\lambda(x:A'.B').M,N) \equiv M[N/x] : B[N/x]} \\ \\ \frac{\Gamma, y:A \vdash App^{x:A.B}(M,y) \equiv App^{x:A.B}(M',y) : B[y/x]}{\Gamma \vdash M \equiv M' : \Pi(x:A).B } \\ \\ \frac{\Gamma \vdash A \equiv A' type \qquad \Gamma, x:A \vdash B \equiv B' type}{\Gamma \vdash \Pi(x:A)B \equiv \Pi(x:A')B' type} \\ \\ \frac{ \Gamma \vdash A \equiv A' type \qquad \Gamma, x:A \vdash B \equiv B' type \qquad \Gamma, x:A \vdash M \equiv M' : B } {\Gamma \vdash \lambda(x:A.B).M \equiv \lambda(x:A'.B').M' : \Pi(x:A).B} \\ \\ \frac{ \Gamma \vdash A \equiv A' type \qquad \Gamma, x:A \vdash B \equiv B' type \qquad \Gamma \vdash M \equiv M' : \Pi(x:A)B \qquad \Gamma \vdash N \equiv N' : A } {\Gamma \vdash App^{x:A.B}(M, N) \equiv App^{x:A'.B'}(M', N') : B[N/x]} \end{gathered}

Valid Contexts and Telescopes

A (raw) telescope Δ\Delta is a (raw) context. A valid telescope ΓΔok\Gamma \vdash \Delta ok is defined by another inductively-defined judgment form:

Γok\frac{}{\Gamma \vdash \cdot ok}
\,
ΓΔokΓ,ΔAtypexΓ,ΔΓΔ,x:Aok\frac{\Gamma \vdash \Delta ok \qquad \Gamma,\Delta \vdash A type \qquad x \notin \Gamma,\Delta} {\Gamma \vdash \Delta,x:A ok}

Intuitively, a telescope is an open context. So a valid context can now be formalized as the closed special case of a valid telescope, with the single-rule judgment form:

ΓokΓok\frac{\cdot \vdash \Gamma ok}{\Gamma ok}

A valid telescope can also be understood as a valid multi-step context extension. So we have the theorem:

(Γok\Gamma ok and ΓΔok\Gamma \vdash \Delta ok) if and only if Γ,Δok\Gamma,\Delta ok.

You can also concatenate telescopes:

(ΓΔok\Gamma \vdash \Delta ok and Γ,ΔΔok\Gamma,\Delta \vdash \Delta' ok) if and only if ΓΔ,Δok\Gamma \vdash \Delta,\Delta' ok.

In fact, by the definition of context validity, the multi-step context extension is a special case of telescope concatenation.

Bidirectional vs Unidirectional

As noted above, there is a canonical correspondence between our bidirectional theory (with any choice of type formers) and a unidirectional one obtained by collapsing both typing judgments TAT\Leftarrow A and TAT\Rightarrow A into one T:AT:A (and thereby the mode-switching rule into the conversion rule).

In fact, we can prove that ΓTA\Gamma \vdash T\Leftarrow A is derivable bidirectionally if and only if ΓT:A\Gamma \vdash T: A is derivable unidirectionally.

The “only if” direction is easy: just change all the \Leftarrows and \Rightarrows to colons in a bidirectional rule to obtain a unidirectional one. For “if”, it suffices to show that all the unidirectional rules translate to admissible bidirectional rules under (T:A)(TA)(T:A)\mapsto(T\Leftarrow A). Each type-former rule in fact translates to a derivable rule: follow the corresponding bidirectional rule (whose conclusion is synthesizing) by the mode-switching rule applied to reflexivity. The only thing requiring a bit of thought is the conversion rule: we want to show that

ΓTAΓABtypeΓTB \frac{\Gamma \vdash T\Leftarrow A \qquad \Gamma \vdash A\equiv B \, type}{\Gamma \vdash T\Leftarrow B}

is admissible in our bidirectional theory. But as noted above, any derivation of ΓTA\Gamma \vdash T\Leftarrow A must end with an invocation of the mode-switching rule. So there must be some CC, such that ΓTA\Gamma \vdash T\Leftarrow A was derived by

ΓTCΓCAtypeΓTA. \frac{\Gamma \vdash T\Rightarrow C \qquad \Gamma \vdash C\equiv A \, type}{\Gamma \vdash T\Leftarrow A.}

So the premises of that rule instance must be derivable. Thus, we can combine the derivations of ΓCAtype\Gamma \vdash C\equiv A \, type and ΓABtype\Gamma \vdash A\equiv B \, type with transitivity, then apply the mode-switching rule

ΓTCΓCBtypeΓTB \frac{\Gamma \vdash T\Rightarrow C \qquad \Gamma \vdash C\equiv B \, type}{\Gamma \vdash T\Leftarrow B}

to get a derivation of ΓTB\Gamma \vdash T\Leftarrow B as desired.

Admissible rules

Inversion lemmas

Inversion lemmas let you “take apart” a derivation by observing that only certain rule(s) could’ve been used as the last step of the derivation, based on the form of one or more objects being judged.

TODO

Structural rules

Writing Γ𝒥\Gamma \vdash \mathcal{J} for one of the judgments, the following rules are admissible by mutual induction on derivations :

ΓΓΓ,Γ𝒥Γ,x:A,Γ𝒥 \frac{\Gamma \vdash \Gamma' \qquad \Gamma, \Gamma' \vdash \mathcal{J}}{\Gamma, x:A, \Gamma' \vdash \mathcal{J}}
\,
ΓBtypeΓ,x:A,y:B,Γ𝒥Γ,y:B,x:A,Γ𝒥 \frac{\Gamma \vdash B\,type \qquad \Gamma, x:A, y:B, \Gamma' \vdash \mathcal{J}}{\Gamma, y:B, x:A, \Gamma' \vdash \mathcal{J}}
\,
Γ,x:A,y:A,Γ𝒥Γ,x:A,Γ[x/y]𝒥[x/y] \frac{\Gamma, x:A, y:A, \Gamma' \vdash \mathcal{J}}{\Gamma, x:A, \Gamma'[x/y] \vdash \mathcal{J}[x/y]}
\,
ΓTAΓ,x:A,Γ𝒥Γ,Γ[T/x]𝒥[T/x] \frac{\Gamma \vdash T \Rightarrow A \qquad \Gamma, x:A, \Gamma' \vdash \mathcal{J}}{\Gamma, \Gamma'[T/x] \vdash \mathcal{J}[T/x]}

(TODO)

Sanity check

Sanity checks are theorems about the formal judgments that provide some confidence that the rules are propagating validity presuppositions correctly. Since we have only one judgment form that establishes any of its presuppositions, there seems to be only one sanity check we can do:

If Γok\Gamma ok and ΓMA\Gamma \vdash M \Rightarrow A then ΓAtype\Gamma \vdash A type.

Intuitively, a derivation ΓMA\Gamma \vdash M \Rightarrow A somehow contains a derivation of the presupposition ΓAtype\Gamma \vdash A type, but the derivation only makes sense when the other presupposition, Γok\Gamma ok, of this judgment form, has been independently established. For example, the variable rule intuitively punts the derivation of type validity to the independent derivation of context validity.

The proof is by induction on the main derivation—of ΓMA\Gamma \vdash M \Rightarrow A—and makes use of the admissible substitution rule:

TODO

Last revised on October 11, 2024 at 14:59:25. See the history of this page for a list of all contributions to it.