# Can a typing judgment admit essentially different derivations?

In any sort of type theory, there are a bunch of rules for constructing derivations of typing judgments such as $x:A,\; y:B(x) \;\vdash\; z:C(x,y)$. (I intend to include also judgments of the form $B:\mathrm{Type}$.) It's certainly possible to get to the same typing judgment using different derivations; for instance I could introduce an unnecessary variable with weakening, then substitute any term for that variable. But it feels as though such a derivation should be "$\beta$-equivalent" to a derivation which omits the unnecessary variable and substitution. So my question is:

Is there a tractable (e.g. inductively generated) equivalence relation on derivations under which all derivations of the same typing judgment become equivalent?

Although I want the answer to be yes, I suspect that it is no, because derivations are a lot like proofs, and I know that at least in intuitionistic logic, there can be multiple "essentially distinct" proofs of a given statement. If so, could it be true for some restricted class of type theories? Can one quantify its falsity?

Edit: Apparently there was a lot of room for misinterpretation of this question! To clarify: I was only talking about type theories in which inhabitation of types is witnessed by a specified term, as in the example typing judgment I gave above. (If you think of types as propositions and terms as proofs, then the question becomes "are all ways to derive a given proof-term equivalent?" But I don't generally tend to think of types only in that way.) Neel's answer seems to say: yes, as long as the type theory satisfies cut-elimination. Whether or not a given type can be inhabited by multiple distinct terms (e.g. one proposition can admit multiple distinct proofs) is a different question.

Edit 2: Maybe if I explain the origin of my question, it will make clearer what I was asking. When trying to define a semantics of DTT in a locally cartesian closed category, it seems to me that the natural approach is to define the interpretation of each type and term inductively using the corresponding categorical constructions, as in D4.4 of Sketches of an Elephant. Unfortunately, this doesn't quite work, because for instance substitition is "strict" in type theory, but pullback is only up to isomorphism in a category.

It seems that the standard way to deal with this is to first strictify the pullbacks in the lccc, e.g. by replacing its codomain fibration by a split one and maybe some additional data (people talk about "comprehension categories" and suchlike). However, looking at the direct construction that doesn't work, it seems to me that it can be interpreted meaningfully as an inductive construction acting not on types+terms, but rather on derivations of typing judgments. If that's right, it seems like one could then get a meaningful interpretation of type theory in an lccc by proving that any two derivations of the same typing judgment produce canonically isomorphic interpretations in the lccc. But that would require a notion of equivalence between derivations which is tractable (so that one can show that any equivalence of derivations gives an isomorphism in the lccc) and under which all derivations can be shown to be equivalent; hence my question.

-
Can one pick a random ambiguous grammar for a language and simulate it in types? –  Mariano Suárez-Alvarez Oct 20 '10 at 17:48

This property is called "coherence", and no, it doesn't always hold.

Establishing this property holds for a given semantics of proofs is a proof obligation. An example of when it doesn't arises with coercive subtyping -- if the diagrams corresponding to possible coercions do not all commute, then the semantics is not coherent, in that the meaning of a term depends critically on its typing derivation. If all you have is the term and knowledge that it has a typing derivation, you can't tell what it means, necessarily.

For a proof-theoretic characterization, the thing to look for is a cut-elimination theorem. One way of reading the cut-elimination theorem is precisely that it says that eliminating intro/elim and elim/intro pairs (i.e., $\beta$ and $\eta$ equations) induces a genuine equivalence relation on proofs.

However, we can still have essentially different proofs. For example, $x : A \land A \vdash \pi_1(x) : A$ and $x : A \land A \vdash \pi_2(x) : A$ are two different proofs that $A$ and $A$ entails $A$. However, cut-elimination guarantees that the addition of proof terms does make the typing derivations unique -- any proof of this entailment must be equal to one or the other, since every proof is equivalent to a cut-free proof, and these are the only two cut-free proofs, and the proof terms let us distinguish the two possibilities.

EDIT: There must be a treatment of this subject in somebody's book (Barendregt?), but I don't know off-hand, since I learned it via osmosis. Probably the best reference I can point you at is Jan Schwinghammer's paper "Coherence of Subsumption for Monadic Types", which nicely illustrates the idea, and whose references also contain pointers to the best available literature.

Noam quite rightly points out that you might actually be interested in the case where all derivations of a judgement are equivalent. (This possibility honestly hadn't even occurred to me, since I'm too intuitionistically contaminated.) The keyword to search for in this case is "proof irrelevance", and I recommend Awodey and Bauer's paper "Propositions as [Types]".

EDIT 2: When cut-elimination holds, then the derivations of a calculus with proof terms become equivalent. If you don't have proof terms, then you can't guarantee equivalence of derivations.

For example, suppose we erased the proof terms from the derivation above, so that we simply had the judgment $A \land A \vdash A$. In this case, even if we know that this judgment holds, we still don't know whether the proof used the left or the right $A$, which are the two intrinsically different derivations of the same judgment. On the other hand, if we have proof terms, then we have a judgment $x : A \land A \vdash e : A$. In this case, the derivation does bebgcome unique, because now we can $\beta\eta$-normalize $e$ and just check whether it is equal to $\pi_1(x)$ or $\pi_2(x)$.

This is why lambda-calculus expressions are called "proof terms": these terms are evidence to establish which proof you meant.

To connect this back with proof irrelevance, a type is "proof irrelevant" when all the proof terms of that type are equivalent. That is, if $\Gamma \vdash e : A$ and $\Gamma \vdash e' : A$, then we know that the two derivations are equivalent, regardless of $e$ and $e'$. For example, the unit type $1$ is proof irrelevant, since every term in it is equivalent to the unit value $\left<\right>$.

-
Thank you very much, this is exactly the sort of thing I wanted. Where is a good reference to read about this? –  Mike Shulman Oct 20 '10 at 21:41
Wait a minute, so when you said "this property holds" you weren't actually referring to the property I was explicitly asking about, namely "all derivations become equivalent"? I thought that was what "cut-elimination guarantees that the addition of proof terms does make the typing derivations unique" meant. –  Mike Shulman Oct 21 '10 at 19:41
If not all derivations are equivalent, can you give an example of two intrinsically different derivations of the same typing judgment (not using subtypes or anything fancy, just in ordinary type theory)? –  Mike Shulman Oct 21 '10 at 19:55
Okay, my first interpretation of your answer was correct, and it is in fact what I want. Thanks! The Schwinghammer paper doesn't help me much, though, because it is mostly about subtyping, but I'd like to see an explanation in the simple case of ordinary typed lambda-calculus, or even better for Martin-Lof DTT. –  Mike Shulman Oct 21 '10 at 23:52

So reading your responses to Neel's answer and to my other answer, I see the important point is that you are making a distinction between proofs/terms and typing judgments. This does not go without saying! Indeed, this is often seen as a "design decision" (though I wouldn't put it that way) in defining a type theory: either directly identify types with propositions and well-typed terms with proofs in a logic, or first define an untyped syntax of terms and then an auxiliary typing judgment. In reality I would say there isn't so much a dichotomy as a hierarchy, with different levels of "types": a good reference for this is Frank Pfenning's "Church and Curry: Combining Intrinsic and Extrinsic Typing". But the fact that it is seen as a design decision (e.g., the simply-typed lambda calculus is presented in both styles) suggests that often the answer to your question is positive: if a typing system can be rephrased directly as a logic, then the types were already in a sense "typing-irrelevant".

Although I want the answer to be yes, I suspect that it is no [....] Can one quantify its falsity?

So conversely I would say that it is false to the extent that you really do need to define a hierarchy of types and "refinement types" (in the terminology of Pfenning). As mentioned in the article for example, this seems to be the case for intersection (and union) types...so let's look at that situation.

To establish the notation: given a type $A$ and two refinement types $S,T\sqsubseteq A$ (e.g., $A = {\mathbb N}$, $S = \it{odd}$, $T = \it{prime}$), we can form the intersection $S\cap T\sqsubseteq A$; the introduction rule for $\cap$ says that a term $M$ of type $A$ has an intersection type $M:S\cap T$ if both $M:S$ and $M:T$, and the two elimination rules go in the opposite direction. Then adapting Neel's example, there are seemingly two different typing derivations of $x : S \cap S \vdash x : S$. On the other hand, it's not clear that we should really distinguish these two derivations. Indeed, part of the idea of having a second layer of refinement types is that we do not assign typing derivations any computational content---so that could be another way of dodging your question.

Does that get at what you were asking? I think the point is that the basic definitions of type theory are still not so clear.

-
I'm ashamed to say I can't make heads or tails of what you're talking about here. I don't necessarily want to identify types with propositions (I like to think of types as sets and terms as elements, or more generally interpret them in some other lccc), but neither do I usually think of defining a syntax of untyped terms first. In what sense are those opposites? They seem to me orthogonal questions: the first is about the intended semantics, and the second is about a syntactical choice. –  Mike Shulman Oct 22 '10 at 0:03
FYI, I edited the question trying to clarify what I was asking and why. –  Mike Shulman Oct 22 '10 at 0:14
The basic question is what are typing judgments about? Do (typed/untyped) terms have any semantic status independent of typing derivations? If they do, good, then we can ask about the "coherence" property at the level of the intended semantics. If they don't, then the property can only be stated at the level of syntax...which to me is a sign of a mismatch: either we should change the syntax to eliminate the distinction between terms and typing derivations (e.g., rephrase simply-typed lambda calculus as intuitionistic natural deduction), or we should refine the semantics. –  Noam Zeilberger Oct 22 '10 at 9:23
That makes sense to me, although in my case (see Edit 2 above) it seems that the desired semantics (lccc's) is "known to be coherent," and the problem is rather how to reflect this coherence in the syntax in order to formally define the semantics. But how is that related to the answer you gave above, in which you talked about "rephrasing a typing system as a logic"? –  Mike Shulman Nov 7 '10 at 5:32
Maybe it would clarify my question if I say that I don't want to treat terms as having any semantic status independent of a typing judgment, but given a term with a typing judgment, I don't want its semantic status to depend on how the typing judgment was arrived at. More specifically, given a definition of a semantics which appears to depend on how a typing judgment was arrived at, I want a systematic way to verify that it doesn't actually depend on that, only on the judgment itself. –  Mike Shulman Nov 7 '10 at 5:53

Proof irrelevance does hold for a restricted class of types. In particular, it's trivially true for the empty type 0 and the singleton type 1, and in dependent type theories more generally for type families denoting decidable properties: $$P(t) = \begin{cases}1 & \text{if }\phi(t)\cr 0 & \text{if }\neg\phi(t)\end{cases}$$ Moreover, the so-called "negative" type constructors give a way of composing proof irrelevant types: the product $A\times B$ is proof irrelevant if both $A$ and $B$ are, and the function space $A\to B$ is proof irrelevant if $B$ is (irrespective of $A$).