Types and membership

typehood

Essentially types are collections of terms. This is how they look from ``outside the theory.'' Inside the theory we see types as methods of construction; to specify a type is to say how to build a certain category of mathematical object. In order to say anything interesting about these objects, we need also to say when we regard two of them as equal. We follow Martin-Löf's method for doing this.

Definition: To specify a type

• Designate a canonical name for it (type is a value)
• Say how canonical elements are formed (a method of construction is specified)
• Say when two elements are equal

Definition: Membership

If A is a type, then $a\in A$ means that $a evals\_to a'$ and a' canonical of type A. Since A is a type, we know what its canonical members are.

Examples of type constructionA new type Let 1 be a type, the unit type Let $\bullet$ be a value in 1, equal to itself, $\bullet=_1\bullet$ or write $\bullet=\bullet$ in 1.

product(1; 1) is a type pair($\bullet$; $\bullet$) is an element function(1; 1) is a type $\lambda$(x.x) $\lambda$(x.$\bullet$) are elements.

Also, $\lambda$(x.x)= $\lambda$(x.$\bullet$) in function(1; 1)

Membership

The notion of type membership, written $a\in A$ for A a type, is defined by the mutually recursive inductive definition of typehood given above. It is easy to see that membership is not decidable.

Let $\Phi_i$ be the ith Turing machine in some acceptable indexing,

Define

H_i(x):=if $\Phi_i(i)$ halts in x steps then void else 1 fi

$\lambda(x.\bullet) \in x:N\rightarrow H_i(x)$ iff $\Phi_i(i)$ diverges