Vtyjkyuk

I want to introduce (dependent) type theory to some friends having background in mathematical logic and set theory.
To make this introduction easy I would like to give an informal presentation that describes types as collection and terms as elements of the types.

My plan was to present type systems as algebraic systems where types are sorts, constructors and eliminators are operations between these sorts and $beta$ and $eta$-reductions are equations that these algebras are required to satisfy.

Unfortunately I'm facing the following problem: I can find a way to describe $lambda$-abstraction (the constructor for function types) in this algebraic framework. The reason is that the inference rule describing $lambda$-abstraction, is in the form
$$beginarrayc Gamma, x colon A vdash y : B \ hline Gamma vdash lambda x colon A. y colon A to Bendarray$$
that uses terms with non empty context $Gamma, x colon A vdash y colon B$.

The problem lies in how to (intuitively) interpret terms with non emtpy context in this algebraic framework: constant terms, i.e. terms with empty context, can be interpreted very naturally as the elements of the types.

So the question is:

What could be an intuitive interpretation of terms with non empty context in an algebraic framework as the one outlined above?

Some remarks to be pointed out at the beginning:

1. Type theory should be thought of as a general mathematical theory of constructions: how mathematical objects are constructed, what are different kinds of constructions (functions, pairs, inductive constructions, co-inductive constructions, etc.), what equational laws they satisfy, and how they can be generally handeled. Thus we should expect a systematic way of introducing new kinds of constructions. Indeed, as we shall see every new way of constructing types follows the same path: formation rules, introduction rules, elimination rules, congruence rules, and equations which explain how the introduction and eliminations fit together.




2. Classical mathematics rests on two pillars: first-order logic and set theory. Set theory is formulated using first-order logic. In contrast, type theory stands on its own. There is no logic beneath type theory. In fact, we can see type theory as a common unification of logic and set theory: certain types are like logical propositions, some types are like sets, and there are also types which are like nothing they have seen before.




3. Because there is no logic, only a formalism for constructing stuff, one has to get used to a new way of speaking and thinking. In type theory it is impossible to say or think "$P$ is true" because the only mechanism available is construction of an element of a type. Since $P$ is a (special kind of) type, we should instead say "we construct an element $e$ of type $P$". (In first-order logic the element $e$ would correspond to a proof of $P$.)




4. Therefore, since in type theory it is impossible to state that a proposition $P$ holds without actually giving a proof $e$ of it, proofs are unavoidable. Or to put it in another way, proofs are "first-class citizen", as they are just elements of certain types. The situation in ordinary math is quite different: even though proofs are central to mathematics, nobody ever considered the set of all proofs of a propostion $P$, or anything like that.

After having spent sometime thinking about this problem I've found the solution (this solution came to my mind after thinking to the semantics of type theory in categories):

If one interprets terms with empty context as elements of the collections/types then terms with non empty context can be naturally interpreted as operation between types.
In details: one can reguard a context $Gamma equiv x_1 colon A_1, x_2 colon A_2 dots x_n colon A_n$ as a sort of cartesian product (not to be confused with the product type, that comes equipped of projections [eliminators]), then a term $Gamma vdash t colon T$ can be interpreted as an operation that associates to every $n$-tuple of elements $a_1 in A_1, dots , a_n in A_n$ an element $t(a_1,dots,a_n) in T$ (or $T(a_1,dots,a_n)$ in the case of dependent types).

With this interpretation in mind the $lambda$-abstraction becomes an higher-order operator that takes operations of the form $Gamma, x colon A vdash t colon B$ into operations of the form $Gamma vdash lambda x colon A. t colon A to B$.

Of course one have to keep in mind the distinction between a term in context $x colon A vdash t colon B$ (that in this interpretation would be an operation between the types $A$ and $B$) and the term $vdashlambda x colon A. t colon A to B$ that is a constant.

From a programming perspective the term $x colon A vdash t colon B$ is a function that takes as input a value of type $A$ and return a value of type $B$ while the term $lambda x colon A. t colon A to B$ is a value of the type $A to B$ that represents the function $t$ internally to the programming language (it is the code of the function $t$).