What I (think) I know:
Type theory is a game where you construct trees from strings. As far as I can tell, the rules of the game are roughly those of a Gentzen system whose "propositions" are typing statements of the form $t:T$, where $t$ is a term variable and $T$ is a type variable.
As in a Gentzen system, trees are constructed inductively by
$$S\to\cfrac SS\ \mid\ \cfrac{S\qquad S}S$$
The nodes are produced according to the formation rules for typing statements
\begin{align*} S&\to l\vdash t:T\\ l&\to \epsilon\ \mid\ \tilde lt:T\\ \tilde l&\to\epsilon\ \mid\ t:T,l\\ t&\to v\ \mid\ (t\ t)\ \mid\ \lambda v.t\\ v&\to x\ \mid\ v'\\ \end{align*}
The types ($T$) are given by some auxiliary system - a finite list of types, base types and constructors, an inductively defined set of types, etc. Additionally, the base game comes standard with the rules
$$\cfrac{\Gamma\vdash M:A\to B\qquad \Gamma\vdash a:A}{\Gamma\vdash Ma:B}\qquad\qquad\cfrac{\Gamma,x:A\vdash M:B}{\Gamma\vdash\lambda x.M:A\to B}\qquad\qquad\cfrac{\Gamma\vdash M:A}{M[x:=y]:A}$$
where, in the last rule, $x$ is a bound variable of $M$ and $y$ does not occur in $M$. Additionally, the base game comes with the rewrite rule $(\lambda x.M\ a)\to M[x:=a]$.
Note: I'm leaving bound variables in $\lambda$-terms untyped because the type of each bound variable is given in the typing statement - i.e. $\lambda x.M:A\to B$ implicitly means $\lambda x:A.M$ since any other type assignment would break the rules (e.g. $\lambda x:C.M:A\to B$, where $C\ne A$).
If any of this is wrong, please correct me.
What I don't know:
- In general, type statements seem to function as hypotheses or inputs, even when put in front of the turnstile. That is, if we introduce $\vdash 0:\mathtt{nat}$, $\vdash S:\mathtt{nat}\to\mathtt{nat}$, and derive the conclusion $\vdash S0:\mathtt{nat}$, we are saying that given the assignment of $0$ to type $\mathtt{nat}$ and $S$ to type $\mathtt{nat}\to\mathtt{nat}$, we can derive "$S0$ is of type $\mathtt{nat}$". The fact that we can replace each of "$0$" and "$S$," and "$\mathtt{nat}$," with an arbitrary term and type, respectively, without changing anything reinforces this point. However, because type assignment is not propositional, there is also no way to negate, disable, or otherwise refute $\vdash-1:\mathtt{nat}$. Yet, most people seem to disagree with this type assignment as though it had the capacity to be "false". In order to reconcile this, the rules of any type theory with a type "$\mathtt{nat}$" must be construed in such a way that $\vdash-1:\mathtt{nat}$ is prevented from forming in the first place. I see no way to do this if we are not already under the "hypotheses" $\vdash-:A$ for types $A\ne\mathtt{nat}\to\mathtt{nat}$ and/or $\vdash 1:B$ for some type $B\ne\mathtt{nat}$. If no such declaration has been made, shouldn't $\vdash -1:\mathtt{nat}$ be just as permissible as $\vdash xy:\mathtt{nat}$, as it occurs in
$$\cfrac{\vdash xy:\mathtt{nat}\qquad\vdash S:\mathtt{nat}\to\mathtt{nat}}{\vdash S(xy):\mathtt{nat}}\qquad?$$
If every type comes equipped with such declarations, shouldn't the "primitive" objects of each type be explicitly provided in its representation somehow, so that I know which terms I am allowed to assign to it?
[As an example of such a representation, we might write $T_1:=\{s_1,\ldots,s_n,f_1:\mathtt{self}\to U_1, f_k:\mathtt{self}\to U_k\}$, where each of $s_1,\ldots,s_n$ is a distinguished term not generated by the grammar of type theory, and $U_1,\ldots U_k$ types (defined analogously to $T_1$) or $\mathtt{self}$. The special symbol $\mathtt{self}$ is needed to ensure that the expansion terminates.
It seems to be taken for granted that each function type comes equipped with some "primitive" functions, which in turn carry some anomalous means of computation, allowing them to be distinguished from arbitrary functions of the same type. This is present, for instance, in Isabelle, Coq, and Haskell, where in addition to providing the typing rules for an introduced function $f$, it is possible to specify a return value for $fx$ distinct from the literal "$fx$". From what I understand, type theories do not generally facilitate computation by means other than the standard rewriting rules already present in the [untyped] lambda calculus. How is it that we end up with named, recursive functions, locked in specific relations to one another when the language provides no means for the construction of such functions? Do we have some auxiliary means of computation which we must provide in addition to the system supplying the population of types?
Certain type constructors require the de-facto existence of functions which map each term of a given type to a type. What is the type of such functions, and how do we construct them without departing from the rules of the game (or invoking the dreaded $\mathtt{type}:\mathtt{type}$)?
(optional) How many auxiliary systems can we tack on to type theory before we're playing a different game altogether? If, at some point, we are simply coding in C++, is it still reasonable to call what we are doing "type theory"? Is category theory type theory? Is set theory type theory? Am I type theory?