nLab pure type system

Contents

Context

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

logicset theory (internal logic of)category theorytype theory
propositionsetobjecttype
predicatefamily of setsdisplay morphismdependent type
proofelementgeneralized elementterm/program
cut rulecomposition of classifying morphisms / pullback of display mapssubstitution
introduction rule for implicationcounit for hom-tensor adjunctionlambda
elimination rule for implicationunit for hom-tensor adjunctionapplication
cut elimination for implicationone of the zigzag identities for hom-tensor adjunctionbeta reduction
identity elimination for implicationthe other zigzag identity for hom-tensor adjunctioneta conversion
truesingletonterminal object/(-2)-truncated objecth-level 0-type/unit type
falseempty setinitial objectempty type
proposition, truth valuesubsingletonsubterminal object/(-1)-truncated objecth-proposition, mere proposition
logical conjunctioncartesian productproductproduct type
disjunctiondisjoint union (support of)coproduct ((-1)-truncation of)sum type (bracket type of)
implicationfunction set (into subsingleton)internal hom (into subterminal object)function type (into h-proposition)
negationfunction set into empty setinternal hom into initial objectfunction type into empty type
universal quantificationindexed cartesian product (of family of subsingletons)dependent product (of family of subterminal objects)dependent product type (of family of h-propositions)
existential quantificationindexed disjoint union (support of)dependent sum ((-1)-truncation of)dependent sum type (bracket type of)
logical equivalencebijection setobject of isomorphismsequivalence type
support setsupport object/(-1)-truncationpropositional truncation/bracket type
n-image of morphism into terminal object/n-truncationn-truncation modality
equalitydiagonal function/diagonal subset/diagonal relationpath space objectidentity type/path type
completely presented setsetdiscrete object/0-truncated objecth-level 2-type/set/h-set
setset with equivalence relationinternal 0-groupoidBishop set/setoid with its pseudo-equivalence relation an actual equivalence relation
equivalence class/quotient setquotientquotient type
inductioncolimitinductive type, W-type, M-type
higher inductionhigher colimithigher inductive type
-0-truncated higher colimitquotient inductive type
coinductionlimitcoinductive type
presettype without identity types
set of truth valuessubobject classifiertype of propositions
domain of discourseuniverseobject classifiertype universe
modalityclosure operator, (idempotent) 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

semantics

Deduction and Induction

Foundations

foundations

The basis of it all

 Set theory

set theory

Foundational axioms

foundational axioms

Removing axioms

Contents

Idea

In type theory, under a pure type system one understand and explicitly typed lambda calculus using dependent product as the type of lambda expressions: the basic idea is that

Γ,x:Ab:B\Gamma, x:A \vdash b:B

implies

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

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.

Definition

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 rules: triples (s 1,s 2,s 3)(s_{1}, s_{2}, s_{3}) of sorts.

    Rules (s 1,s 2,s 2)(s_{1}, s_{2}, s_{2}) are abbreviated as (s 1,s 2)(s_{1}, s_{2}).

Remark

These rules 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.

Remark

In fact all rules (s 1,s 2,s 2)(s_{1}, s_{2}, s_{2}) appearing in the following have s 2=s 3s_2 = s_3. So we can just as well regard RR as a binary relation RS×SR \hookrightarrow S\times S (rather than a ternary one).

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.

namerulecondition
(axioms)c:s\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'}

Examples

Strongly normalizing systems

Intuitionistic (higher-order) logic

Lambda cube

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

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, see Barendregt 91, 2.1)

The other systems omit some of the last three rules. 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 Fyesyes
λω̲\lambda\underline{\omega}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 rules 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 (System U \mathsf{U}^-):

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

References

  • Henk Barendregt, Introduction to generalized type systems, J. Funct. Program. 1(2), 1991 (pdf)

  • 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. (preprint pdf)

Survey includes

  • Frade, Calculus of inductive constructions (pdf)

  • Cody Roux, Pure type systems: Dependents when you need them, talk at Boston Haskell Meetup 2015 (slides,video)

A generalization to cumulativity can be found in

  • Bruno Barras and Benjamin Gregoire, On the role of type decorations in the Calculus of Inductive Constructions, Lecture Notes in Computer Science Volume 3634, 2005, pp 151-166, PDF

Last revised on February 28, 2023 at 14:44:22. See the history of this page for a list of all contributions to it.