Type theory

natural deduction metalanguage, practical foundations

  1. type formation rule
  2. term introduction rule
  3. term elimination rule
  4. computation rule

type theory (dependent, intensional, observational type theory, homotopy type theory)

syntax object language

computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory

logiccategory theorytype theory
trueterminal object/(-2)-truncated objecth-level 0-type/unit type
falseinitial objectempty type
proposition(-1)-truncated objecth-proposition, mere proposition
proofgeneralized elementprogram
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
cut elimination for implicationcounit for hom-tensor adjunctionbeta reduction
introduction rule for implicationunit for hom-tensor adjunctioneta conversion
logical conjunctionproductproduct type
disjunctioncoproduct ((-1)-truncation of)sum type (bracket type of)
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
existential quantificationdependent sum ((-1)-truncation of)dependent sum type (bracket type of)
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
completely presented setdiscrete object/0-truncated objecth-level 2-type/preset/h-set
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
modalityclosure operator, (idemponent) monadmodal type theory, monad (in computer science)
linear logic(symmetric, closed) monoidal categorylinear type theory/quantum computation
proof netstring diagramquantum circuit
(absence of) contraction rule(absence of) diagonalno-cloning theorem
synthetic mathematicsdomain specific embedded programming language

homotopy levels




A question that is traditionally of some debate in type theory is,

What does it mean for a term to have more than one type?

One place where this question becomes relevant is in the interpretation of polymorphism. Another is for type systems with a non-trivial subtyping? relation, in which case it becomes pertinent to consider the meaning of the subsumption rule:

e:AABe:B\frac{e:A \qquad A \le B}{e:B}

One possibility (sometimes called the inclusion interpretation of subtyping) is based on the idea of interpreting types as properties of terms (what is also sometimes called “types à la Curry”, or the extrinsic view of typing). Under this interpretation, the subsumption rule can be read more or less literally, as asserting that if ee satisfies the property AA, and AA entails BB, then ee also satisfies the property BB. One potential drawback of this interpretation, though, is that it seems to commit you to giving a meaning to “untyped” terms (although these terms may of course intrinsically have some more coarse-grained type structure, as in models of pure lambda calculus by reflexive objects).

A different possibility (sometimes called the coercion interpretation of subtyping) is to read the subsumption rule as introducing an implicit coercion from AA to BB. Under this interpretation, subtyping can be seen as simply providing a convenient shorthand notation, when having to write out these coercions explicitly would be too burdensome. This interpretation allows one to maintain an intrinsic (“à la Church”) view of typing, but on the other hand it introduces a subtle issue of coherence: if there is more than one way of deriving the subtyping judgment ABA \le B, we would like to know that all of these result in equivalent coercions from AA to BB, so that the meaning of a well-typed term is independent of its typing derivation.

In dependent type theory

Consider a dependent proposition A:Type,x:AP(x):PropA: Type, x:A \vdash P(x):Prop. Then the dependent sum, x:AP(x)\sum_{x:A} P(x), may be thought of as ‘AAs which are PP’. Sometimes it is convenient to identify a term of this dependent sum as though it were a term of the full type AA. Here we can use the first projection of the dependent sum to coerce the identification.

For example, we might have introduced ‘Eve’ as a term of type WomanWoman, and then wish to form a type Relatives(Eve)Relatives(Eve), when Relatives(x)Relatives(x) had been introduced as a type depending on x:Humanx: Human. If WomanWoman had been defined as x:HumanFemale(x)\sum_{x:Human} Female(x), then EveEve has projections to the underlying human and to a warrant for Eve’s being female. It would be clumsy to insist on Relatives(π 1(Eve))Relatives(\pi_1(Eve)). Coercion along this projection allows us to form Relatives(Eve)Relatives(Eve).

Luo (1999) proposed a way of formalizing coercions in dependent type theory, through what he calls the coercive definition rule, which when generalized to allow dependency on the coerced term is:

Γ,x:Bf(x):C(x)Γa:AΓA< cB:TypeΓf(a)=f(c(a)):C(c(a)) \frac{\Gamma, x: B \vdash f(x) : C(x) \; \; \; \Gamma \vdash a : A \;\;\;\Gamma \vdash A \lt_{c} B : Type}{\Gamma \vdash f(a) = f(c(a)) : C(c(a))}

In this notation, a coercion between two types AA and BB is denoted A< cBA \lt_{c} B, for c:(AB)c: (A \to B).


In homotopy type theory, the inclusion of a smaller universe in type theory in a larger one is often considered as a coercion.


Reynolds (2000) gave an interesting proof of coherence for a coercion interpretation of a language with subtyping. The proof works by first building a logical relation between this “intrinsic semantics” and a separate untyped semantics of the language (the latter based on interpreting programs as elements of a universal domain UU), and then establishing a “bracketing theorem” which says that for any domain [[A]][[A]] in the image of the intrinsic semantics, there are a pair of functions ϕ A:[[A]]U\phi_A : [[A]] \to U and ψ A:U[[A]]\psi_A : U \to [[A]] such that

  • for any a[[A]]a\in [[A]], aa is logically related to ϕ A(a)\phi_A(a)
  • if aa is logically related to xx, then a=ψ A(x)a = \psi_A(x)

Combined, the logical relations theorem and the bracketing theorem imply that the coercion [[α]]:[[A]][[B]][[\alpha]] : [[A]] \to [[B]] associated to any derivation α\alpha of a subtyping judgment ABA \le B can be factored as

[[A]] ϕ A U ψ B [[B]] \begin{matrix} [[A]] &\overset{\phi_A}{\to} & U & \overset{\psi_B}{\to} & [[B]] \end{matrix}

and hence in particular that any two derivations α 1,α 2\alpha_1,\alpha_2 of ABA \le B result in the same coercion [[α 1]]=[[α 2]]=(ϕ A;ψ B):[[A]][[B]][[\alpha_1]] = [[\alpha_2]] = (\phi_A;\psi_B) : [[A]] \to [[B]].

  • subtype?


  • John C. Reynolds, Using Category Theory to Design Implicit Conversions and Generic Operators, In Proceedings of the Aarhus Workshop on Semantics-Directed Compiler Generation (January 14-18, 1980), Springer-Verlag. (pdf)

  • John C. Reynolds, The Coherence of Languages with Intersection Types. TACS 1991. (ps)

  • John C. Reynolds, The Meaning of Types: from Intrinsic to Extrinsic Semantics. BRICS Report RS-00-32, Aarhus University, December 2000. (pdf)

  • Zhaohui Luo, Coercive subtyping. Journal of Logic and Computation, 9(1):105–130, 1999. ps file.

  • Zhaohui Luo, Type-Theoretical Semantics with Coercive Subtyping, pdf

Last revised on April 11, 2016 at 06:05:10. See the history of this page for a list of all contributions to it.