This page is part of the Initiality Project.
All our terms are fully annotated. For instance, we write rather than just . 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 and , if can be derived for any value of , then there is a canonical such that can be deduced syntactically, or synthesized, from and . For instance, if has any type, then it must have the type . On the other hand, the conversion rule
implies that must also have any type that is judgmentally equal to . 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 example, it synthesizes only , up to syntactic equality, but it checks against any type judgmentally equal to .
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 , we have two typing judgments:
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:
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 , thereby generalizing the mode-switching rule to the conversion rule. Below we will make this “isomorphism” a bit more precise.
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 , is called a typing declaration, with being a type to which the variable belongs.
A valid context is a raw context such that each judgment 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 should therefore be “if is a valid context, then holds in that context” (and this is the meaning we will give it semantically).
Our type theory has five judgment forms. Here is a metavariable ranging over raw contexts, while are metavariables ranging over raw terms.
All the metavariables occurring in all of our judgments should be regarded as “inputs”, with the sole exception that in the synthesizing judgment 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 it takes and as inputs and returns 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 need only be “correct” under the assumption that is a valid context and , but in turn these assumptions must ensure that all the analogous “preconditions” of all premises of such rules hold.
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:
The other structural rules of weakening, contraction, and substitution will be admissible.
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 .
This is also the only incarnation of the conversion rule, which in a “unidirectional” system is
A bidirectional system controls this rule more carefully, enforcing it to be used (when and) only when the mode switches.
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 , we take as input that and , so we don’t need any premise in the reflexivity rule, but we do need one in the transitivity rule.
Similarly takes as input that and . It also takes .
TODO. In fact, specifying the constant rules is part of the “signature”.
Each type former (-types, -types, etc.) has a collection of rules giving its
A (raw) telescope is a (raw) context. A valid telescope is defined by another inductively-defined judgment form:
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:
A valid telescope can also be understood as a valid multi-step context extension. So we have the theorem:
( and ) if and only if .
You can also concatenate telescopes:
( and ) if and only if .
In fact, by the definition of context validity, the multi-step context extension is a special case of telescope concatenation.
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 and into one (and thereby the mode-switching rule into the conversion rule).
In fact, we can prove that is derivable bidirectionally if and only if is derivable unidirectionally.
The “only if” direction is easy: just change all the s and s 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 . 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
is admissible in our bidirectional theory. But as noted above, any derivation of must end with an invocation of the mode-switching rule. So there must be some , such that was derived by
So the premises of that rule instance must be derivable. Thus, we can combine the derivations of and with transitivity, then apply the mode-switching rule
to get a derivation of as desired.
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
Writing for one of the judgments, the following rules are admissible by mutual induction on derivations :
(TODO)
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 and then .
Intuitively, a derivation somehow contains a derivation of the presupposition , but the derivation only makes sense when the other presupposition, , 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 —and makes use of the admissible substitution rule:
TODO
Last revised on November 1, 2018 at 19:17:08. See the history of this page for a list of all contributions to it.