nLab
meaning explanation

The meaning explanations of type theory

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

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

semantics

Foundations

The meaning explanations of type theory

Idea

Per Martin-Löf‘s meaning explanations of type theory provide a way to justify the correctness of the rules of type theory. The meaning of the judgements of type theory are defined by computation of closed terms to canonical form in some untyped notion of computation, such as a lambda calculus extended with constants for the constructors and eliminators of type theory.

From a technical/mathematical point of view, the meaning explanations give rise to a realizability model of type theory, where realizers are terms in some untyped notion of computation, such as an extended lambda calculus. That is, it can be regarded as a description of how types are assigned to untyped computations. However, the term “meaning explanations” also refer to the “philosophical” or “pre-mathematical” component, which regards this as an “explanation” of the “constructive validity” of the judgements of the type theory.

The standard meaning explanations validate not just the rules of intensional type theory but also the stronger rules of extensional type theory. Thus, if one regards it as the “intended semantics” then one may believe in the extensional theory. However, like any particular semantics for a formal theory, the meaning explanation also validates many other “rules” as well which are not usually added to type theories, so it is not so clear that meaning explanations in their own right argue for extensionality. They can also be modified so as to no longer satisfy extensionality.

Martin-Löf has been quoted as saying

Some people feel that when I have presented my meaning explanations I have said nothing. And this is how it should be. The standard semantics should be just that: standard. It should come as no surprise.

Definition

Suppose we have given some collection of computational objects which we call “terms”, with an untyped notion of “reduction” or “computation”. These could be terms in a lambda calculus, or elements of a partial combinatory algebra, or even programs in a real-world programming language such as C, Java, or Python. We write xyx\Rightarrow y to mean that xx computes or reduces to yy (in some number of steps). We then define simultaneously the following predicates, where a,b,Aa,b,A are terms:

  • AA is a type, often written AtypeA\;type.
  • aa has type AA, written a:Aa:A.
  • aa and bb are equal elements of type AA, written a=b:Aa=b:A.

The definition is by induction-recursion. We define the property “AA is a type” inductively, and simultaneously we define recursively two functions on such AA, one giving the collection of terms of type AA, and the other giving the collection of pairs of terms considered equal as elements of AA. Note that each such collection may itself be a prior inductive definition.

The definition is intended to satisfy some properties:

  • Equality:

    • a:Aa:A if and only if a=a:Aa=a:A. (Reflexivity)
    • If a=b:Aa=b:A then b=a:Ab=a:A. (Symmetry)
    • If a=b:Aa=b:A and b=c:Ab=c:A then a=c:Aa=c:A. (Transitivity)
  • Reverse reduction:

    • If VtypeV\;type and AVA \Rightarrow V then AtypeA\;type.
    • The other judgment forms similarly respect reverse reduction in all positions.

By reflexivity, the specification of which terms have a type is technically redundant. It is just reiterating the reflexivity instances of equality. So for this meaning explanation, the recursive part of the definition is assigning types their meaning as partial equivalence relations (PERs) on terms.

We expect a:Aa:A if and only if a=a:Aa=a:A, rather than just the one, usual direction because we want equality to only be defined on elements. By symmetry and transitivity, a=b:Aa=b:A implies a=a:Aa=a:A and b=b:Ab=b:A, so then by the unusual direction, a:Aa:A and b:Ab:A.

The reverse reduction properties are saying that the relevant information about a term comes from the value it reduces to. Meaning explanations provide a sense in which type theory is about computational behavior. For this system, the computational behavior of a term is to return a value. Note however that not all terms reduce to a value, for example, the Ω\Omega combinator: (λx.xx)(λx.xx)(\lambda x.x\,x) (\lambda x.x\,x).

The clauses we should include in the inductive-recursive definition depend on what type constructors we want to put into our type theory; in each case the base notion of untyped computation must include corresponding operators. Here are three paradigmatic examples.

Natural numbers

Suppose that we have terms NN, 00, and s(x)s(x), along with a recursor rec(n,z 0,xr.z s)rec(n,z_0,x\,r. z_s) such that

n0z 0vrec(n,z 0,xr.z s)v\frac{n \Rightarrow 0 \qquad z_0 \Rightarrow v} {rec(n,z_0,x\,r.z_s) \Rightarrow v}

and

ns(n)z s[n/x,rec(n,z 0,xr.z s)/r]vrec(n,z 0,xr.z s)v.\frac{n' \Rightarrow s(n) \qquad z_s[n/x,rec(n,z_0,x\,r.z_s)/r] \Rightarrow v} {rec(n',z_0,x\,r. z_s) \Rightarrow v}.

The term rec(n,z 0,xr.z s)rec(n,z_0,x\,r. z_s) is intended to denote the value at nn of a recursively defined function specified to be z 0z_0 at zero and z sz_s at successors. Here xx and rr are variables which may occur free in z sz_s but are bound in rec(n,z 0,xr.z s)rec(n,z_0,x\,r. z_s), representing the predecessor and the result of the last recursive call, respectively.

Then to explain the natural numbers type, we include a clause in the inductive definition of “AA is a type” which says

  • if ANA\Rightarrow N, then AA is a type.

The corresponding clause for elements is

  • if ANA\Rightarrow N, then the collection of terms aa such that a:Aa:A is defined inductively by the clauses:
    • if a0a\Rightarrow 0, then a:Aa:A.
    • if as(b)a\Rightarrow s(b) and b:Ab:A, then a:Aa:A.

Note that the recurrence in this inductive definition doesn’t go via the overall recursive definition of a:Aa:A. In other words, to put the above clause more pedantically, we first define

  • an inductive predicate IsNatIsNat:
    • if a0a\Rightarrow 0, then IsNat(a)IsNat(a).
    • if as(b)a\Rightarrow s(b) and IsNat(b)IsNat(b), then IsNat(a)IsNat(a).

Then say

  • if ANA\Rightarrow N, then the collection of terms aa such that a:Aa:A is those such that IsNat(a)IsNat(a).

The clause for equality is

  • if ANA\Rightarrow N, then the collection of pairs a,ba,b such that a=b:Aa=b:A is defined inductively by the clauses:
    • if a0a\Rightarrow 0 and b0b\Rightarrow 0, then a=b:Aa=b:A.
    • if as(a)a\Rightarrow s(a') and bs(b)b\Rightarrow s(b') and a=b:Aa'=b':A, then a=b:Aa=b:A.

With a similar separation of the inductive definition.

Function types

Suppose that we have a term constructor yielding “ABA\to B” for terms AA and BB, and similarly app(f,a)app(f,a) and λx.t\lambda x.t, such that

fλx.tt[a/x]vapp(f,a)v.\frac{f \Rightarrow \lambda x.t \qquad t[a/x] \Rightarrow v} {app(f, a) \Rightarrow v}.

Then to explain the function type, we include a clause in the inductive definition of “AA is a type” which says

  • if AA is a type and BB is a type and C(AB)C\Rightarrow (A\to B), then CC is a type.

The clause for elements is:

  • if C(AB)C\Rightarrow (A\to B) for types AA and BB, and for any a=a:Aa=a':A we have app(f,a)=app(f,a):Bapp(f,a)=app(f,a'):B, then f:Cf:C. In other words, the collection of elements of type ABA\to B is the collection of terms ff such that for any a=a:Aa=a':A we have app(f,a)=app(f,a):Bapp(f,a)=app(f,a'):B.

For equality, we have:

  • if C(AB)C\Rightarrow (A\to B) for types AA and BB, and for any a=a:Aa=a':A we have app(f,a)=app(g,a):Bapp(f,a)=app(g,a'):B, then f=g:Cf=g:C.

These are not inductive definitions as we had for the natural numbers; they are merely simple definitions. On the other hand, we are now using the fact that the function mapping types to their collections of element pairs is recursively defined, since in order to make this definition, we must invoke it at AA and BB. The negative occurrence of a=a:Aa=a':A in this clause (and similar occurrences in other clauses for higher order types) is the reason why the whole explanation cannot just be defined by mutual induction.

This clause for function types is not the one Martin-Löf proposed. Unlike all of Martin-Löf’s clauses, this one gives all terms of a function type directly; it doesn’t just give the canonical terms first, with the rest defined via reduction. This is because it defines the elements in reference to the elimination form, appapp, instead of the introduction form, λ\lambda, as Martin-Löf did. Here’s Martin-Löf’s clause for elements (adapting for this non-dependent case):

  • if C(AB)C\Rightarrow (A\to B) for types AA and BB, fλx.bf \Rightarrow \lambda x.b for some (variable xx and term) bb, and for any a=a:Aa=a':A we have b[a/x]=b[a/x]:Bb[a/x]=b[a'/x]:B, then f:Cf:C.

The element equality clause gets an analogous change. (Exercise!)

Both styles of function type validate all the usual function rules of extensional type theory.

Identity types

Suppose we have a term constructor yielding Id A(a,b)Id_A(a,b) for terms A,a,bA,a,b, and similarly some term reflrefl. Then to explain the identity type, we add to the inductive definition of “AA is a type” the clause

  • If AA is a type, a:Aa:A and b:Ab:A, and CId A(a,b)C \Rightarrow Id_A(a,b), then CC is a type.

Here we are finally using the fact that typehood and elements are defined by induction-recursion: this clause in the inductive definition of typehood refers to the value of the recursive elementhood function at some smaller type.

The clause for elements is:

  • If AA is a type, a:Aa:A, b:Ab:A, and CId A(a,b)C \Rightarrow Id_A(a,b), then p:Cp:C just if a=b:Aa=b:A and preflp \Rightarrow refl. So, the collection of elements of Id A(a,b)\Id_A(a,b) contains something only if a=b:Aa=b:A, in which case it contains precisely those terms which reduce to refl.

The clause for equality is:

  • If AA is a type and a:Aa:A, b:Ab:A, and CId A(a,b)C \Rightarrow Id_A(a,b), then p=q:Cp=q:C just if a=b:Aa=b:A, preflp\Rightarrow refl, and qreflq\Rightarrow refl.

Because we have deliberately only put reflrefl (and terms reducing to it) into the identity type, this definition of identity types will validate uniqueness of identity proofs (UIP). Moreover, because Id A(a,b)Id_A(a,b) is inhabited if and only if a=b:Aa=b:A, it validates the “equality reflection” rule of extensional type theory.

There are simple ways to modify the meaning explanation so as to no longer validate the extensional rules. For instance, if we add to the semantics additional “free variables”, so that there are “neutral terms” which do not compute to any canonical form, and modify the rules of the interpretation so as to say that any normalizable neutral term inhabits every type, then extensionality will no longer hold, since the identity type (like any type) will contain all the variables. This is maybe not a particularly compelling model of intensionality, but there are proposals for better ways to expand the meaning explanation to deal with intensional type theory.

Other judgements

Type equality

The easy way is to say that

  • A=BA=B means that
    • AtypeA\;type and BtypeB\;type, and
    • for all aa, a:Aa:A if and only if a:Ba:B, and
    • for all aa and bb, a=b:Aa=b:A if and only if a=b:Ba=b:B.

This validates the conversion rules. It’s extensional in a manner similar to material set theory, which seems appealing, given the rest of the setup. But it turns out to be inconvenient in this case, because for technical reasons, many rules will require more premises in order to be valid. So it’s a trade-off. Nuprl uses a more intensional type equality, inductively defining A=BA=B along with AtypeA\;type, to simplify the rules.

Hypothetical judgements

TODO!

Intuitively, open terms are multi-argument dependent functions. The hypothetical judgements are defined in terms of the basic judgements on closed terms by substituting a lot of appropriate closed terms. Respect for equality is enforced in a manner to agree with the function type constructor.

The rules of type theory

The claim is that by inspecting these definitions, one can arrive at the formal rules of type theory for manipulating judgments such as “AA is a type”, “a:Aa:A”, and “a=b:Aa=b:A”, which no longer refer to any given notion of computation. However, Martin-Löf famously wrote

…there are … certain limits to what verbal explanations can do when it comes to justifying axioms and rules of inference. In the end, everybody must understand for himself.

Moreover, as mentioned above, the meaning explanation (like any particular semantics) validates many other “rules” which are not usually added to type theories, such as

x:Id N(0,1)5:NN x : Id_N(0,1) \vdash 5 : N \to N

(However in Nuprl rules such as these are, in fact, included.) Thus, some discrimination is required, as well as some choices (e.g. whether to add the extensionality rule for identity types).

References

  • Per Martin-Löf, Intuitionistic Type Theory (Notes by Giovanni Sambin of a series of lectures given in Padua, June 1980). Napoli, Bibliopolis, 1984. (pdf)

  • Per Martin-Löf, Constructive mathematics and computer programming (pdf)

  • Per Martin-Löf. On the Meanings of the Logical Constants and the Justifications of the Logical Laws, Nordic Journal of Philosophical Logic, 1(1): 11–60, 1996 (pdf)

  • UF-IAS-2012, Meaning Explanations

Proposal for homotopy type theory:

Last revised on April 18, 2019 at 11:36:24. See the history of this page for a list of all contributions to it.