pure type system


Type theory

natural deduction metalanguage, practical foundations

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


syntax object language


logiccategory theorytype theory
falseinitial objectempty type
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
conjunctionproductproduct type
implicationinternal homfunction type
negationinternal hom into initial objectfunction type into empty type
universal quantificationdependent productdependent product type
equivalencepath space objectidentity type
equivalence classquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
setinternal 0-groupoidBishop set/setoid
universeobject classifiertype of types
proof netstring diagramquantum circuit
synthetic mathematicsdomain specific embedded programming language

homotopy levels


Deduction and Induction




A pure type system is an explicitly typed lambda calculus using dependent product as the type of lambda expressions: the basic idea is that

Γ,x:AB:C\Gamma, x:A \vdash B:C


Γ(λx:A.B):(x:A.C).\Gamma \vdash (\lambda x:A . B) : (\prod x:A . C).

In other words a pure type system is

  1. a system of natural deduction;

  2. for dependent types;

  3. and with (only) the dependent product type formation rule specified.


A pure type system is defined by * a set SS of sorts, all of which are constants, * a set AA of axioms of the form c:sc : s with cc a constant and ss a sort, * a set RS×S×SR \hookrightarrow S \times S \times S of relations: triples (s 1,s 2,s 3)(s_{1}, s_{2}, s_{3}) of sorts. Relations (s 1,s 2,s 2)(s_{1}, s_{2}, s_{2}) are abbreviated as (s 1,s 2)(s_{1}, s_{2}).


These relations will appear in the type formation rule for dependent product types below. They will say that for a type of sort s 2s_2 depending on a type of sort s 1s_1 its dependent product is a type of sort s 3s_3.


In fact all such triples appearing in the following have s 2=s 3s_2 = s_3. So we can just as well regard them as binary relations RS×SR \hookrightarrow S\times S (rather than ternary ones).

From the above input data we derive the following

  1. The terms of a pure type system are the following (recursive definition):

    • variables and constants
    • (λx:A.B)(\lambda x : A . B) (abstraction)
    • (x:A.B)(\prod x : A . B) (product)
    • ABA B (application)

    Here xx is a variable and AA, BB are terms. The operators λ\lambda and \prod bind the variable xx.

  2. The typing of terms is inductively defined by the following rules.

    A typing is of the form

    x 1:A 1,,x n:A nA:B x_{1} : A_{1}, \dots, x_{n} : A_{n} \vdash A : B

    meaning that the types of the variables declared on the left induces the term AA has type BB. Note that types are also terms.

    The order of variable declarations is significant: the declaration x i:A ix_{i} : A_{i} may depend on declarations to its left.

The natural deduction rules are defined to be the following, for all sSs \in S and where xx ranges over the set of variables.

(axioms)Γc:s\Gamma \vdash c : sif (c:s)(c : s) is an axiom;
(start)ΓA:sΓ,x:Ax:A\frac{\Gamma \vdash A:s}{\Gamma, x : A \vdash x : A}if xΓx \notin \Gamma
(weakening)ΓA:B;ΓC:sΓ,x:CA:B\frac{\Gamma \vdash A:B; \quad \Gamma \vdash C:s}{\Gamma, x : C \vdash A : B}if xΓx \notin \Gamma
(product)ΓA:s 1;Γx:AB:s 2Γ(x:A.B):s 3\frac{\Gamma \vdash A : s_{1}; \quad \Gamma x:A \vdash B : s_{2}}{\Gamma \vdash (\prod x:A . B) : s_{3}}if (s 1,s 2.s 3)R(s_{1}, s_{2}. s_{3}) \in R;
(application)ΓF:(x:A.B);Γa:AΓFa:B[x:=a]\frac{\Gamma \vdash F : (\prod x:A . B); \quad \Gamma \vdash a : A}{\Gamma \vdash Fa : B [x := a]}
(abstraction)Γ,x:Ab:B;Γ(x:A.B):sΓ(λx:A:b):(x:A:B)\frac{\Gamma, x:A \vdash b : B; \quad \Gamma \vdash (\prod x:A . B) : s}{\Gamma \vdash (\lambda x:A:b) : (\prod x:A:B)}
(conversion)ΓA:B;ΓB:s;B= βBΓA:B\frac{\Gamma \vdash A : B; \quad \Gamma \vdash B' : s; \quad B =_{\beta} B'}{\Gamma \vdash A : B'}


Strongly normalizing systems

Intuitionistic (higher-order) logic

Lambda cube

The lambda cube consists of eight systems arranged in a cube. The most expressive is given by the following choice of sorts, axioms and relations:

symbolactual value
S=S = {*,}\{\ast, \square\}
A=A ={(*:)}\{(\ast : \square)\}
R=R ={(*,*),(*,),(,*),(,)}\{(\ast, \ast), (\ast, \square), (\square, \ast), (\square, \square)\}

(Here {*,}\{\ast, \Box\} denotes the 2-element set.)

The other systems omit some of the last three relations. Some specific systems are the following:

name(*,*)(\ast, \ast)(*,)(\ast, \square)(,*)(\square, \ast)(,)(\square, \square)
λ\lambda\rightarrow simply typed lambda calculusyes
λP{\lambda}P logical frameworkyesyes
λ2\lambda2 system F?yesyes
λC{\lambda}C calculus of constructionsyesyesyesyes

Calculus of constructions

For instance for the calculus of constructions we have

The single axiom *:* \colon \Box hence says that Prop:TypeProp \colon Type, hence that Prop is a type.

The relations express the usual rule for dependent product type:

Inconsistent systems

The most permissive pure type system:

symbolactual value
S=S = {*}\{\ast\}
A=A = {(*:*)}\{(\ast : \ast)\}
R=R = {(*,*)}\{(\ast, \ast)\}

But there is an example with even non-circular system of axioms:

symbolactual value
S=S ={*,,}\{ \ast, \square, \triangle\}
A=A ={(*:),(:)}\{(\ast : \square), (\square : \triangle)\}
R=R = {(*,*),(,*),(,),(,)}\{(\ast, \ast), (\square, \ast), (\square, \square), (\triangle, \square)\}

The calculus of inductive constructions can be formulated as a particular pure type system (with a hierarchy of type of types) augmented by rules for introduing inductive types.


  • Henk Barendregt (Catholic University Nijmegen), Lambda calculi with types?, To appear in Samson Abramsky, D.M. Gabbay and T.S.E. Maibaum (eds.) Handbook of Logic in Computer Science, Volume II, Oxford University Press

A quick survey is in

  • Frade, Calculus of inductive constructions (pdf)

Revised on February 27, 2013 18:36:55 by DAY? (