This will be the Second Post in the PLT section. It will introduce the Lambda Calculus for Types-Dependent-on-Types[${\lambda }_{\omega }$] (or atleast, a version of it) : The Motivation behind it; Its Semantics and Properties.

I expect the reader to be familiar with the basics of Lambda Calculus, Type Theory, and the System $\lambda 2$, which is the Second-Order Typed Lambda Calculus.

Once again, I will use ${\to }_{\beta }$ to refer to singular and chained $\beta$-reductions.

MOTIVATION : Let’s start by motivating the need for (${\lambda }_{\omega }$) and seeing why ($\lambda 2$) isn’t enough for sophisticated types. In order to see this, let’s briefly remind ourselves of the generating Grammars for the set of $𝕋$2-types and ($\lambda 2$) :

$𝕋$2 = $𝕍$ $|$ ($𝕋$2 $\to$ $𝕋$2) $|$ $\prod 𝕍$:$*$.$𝕋$2

${\Lambda }_{𝕋2}$ = V $|$ $\lambda$V:$𝕋$2. ${\Lambda }_{𝕋2}$ $|$ ${\Lambda }_{𝕋2}$ ${\Lambda }_{𝕋2}$ $|$ $\lambda 𝕍$:$*$.${\Lambda }_{𝕋2}$ $|$ ${\Lambda }_{𝕋2}𝕋2$

The $\lambda 2$, as we can see, is great at dealing with Terms-Dependent-on-Types, by introducing the $\prod$-type. This allows a term to "bind" to many different types. However, the bindings are relatively straightforward, and therefore, so are the $\prod$-types.

An example is the definition of the ’Nat’-type :

$\mathbb{N}$ $\equiv$ $\prod \alpha$ : $*$ . $(\alpha \to \alpha )\to \alpha \to \alpha$

All elements of ‘Nat‘ will have this type, and can be constructed generally as : $\lambda \alpha$ : $*$ . $\lambda$f : $\alpha \to \alpha$ . $\lambda$x : $\alpha$ . $f\left(f\right(f(...(fx\left)\right)\left)\right)$

It is easy to see that - $f\left(f\right(f(...(fx\left)\right)\left)\right)$ : $\alpha$

So, $\lambda 2$ gives us the ability to concisely write functions with terms for generic types. For instance, one could construct a generic identity function, and then simply substitute in the type and term (in that order), to make it act as an identity function for that specific Type. However, it doesn’t allow us to construct Types-Dependent-on-Types. The reason for this is in the 2nd-order application/abstraction rules in $\lambda 2$ :

As on can see, the $\Gamma ⊢B:*$ proposition from $\left(app{l}_2\right)$ does not allow us to "bind" more complicated types than $*$. In addition, the cycle for this simplicity is completed because $\left(abs{t}_2\right)$ only allows us to introduce and make polymorphic some $\alpha$ with $*$.

This limits the expressiveness of $\lambda 2$. Here, we can have variables $x,y,...$ that are dependent on some $\alpha ,\beta ,..$, but we can’t have some arbitrary type be dependent on another type.

Specifically, expressions of the sort :

i) $\lambda \alpha$ : $*$ . $\alpha \to \alpha$

ii) $\lambda \alpha$ : $*$ . $\lambda \beta$ : $*$ . $\alpha \to \beta$

are not possible in $\lambda 2$.

Ideally, we would like these expressions to become placeholders for more generic types via $\beta$-reduction :

i) $(\lambda \alpha$ : $*$ . $\alpha \to \alpha )\gamma$ ${\to }_{\beta }$ $\gamma \to \gamma$

ii) $(\lambda \alpha$ : $*$ . $\alpha \to \alpha )\delta$ ${\to }_{\beta }$ $\delta \to \delta$

iii) $(\lambda \alpha$ : $*$ . $\alpha \to \alpha )({\tau }_1\to {\tau }_2)$ ${\to }_{\beta }$ $({\tau }_1\to {\tau }_2)\to ({\tau }_1\to {\tau }_2)$

We can see that these allow us to substitute types into types. This is a very useful abstraction upon which many modern functional programming constructs rely. Monads, for example, often rely on implicitly Dependent-Types.

However, none of this machinery is possible in $\lambda 2$, and we shall need new Semantics to introduce them : Enter ${\lambda }_{\omega }$.

SEMANTICS : Now that we know what shortcomings we had before, and what new expressive abilities we would like in our system (vaguely), let us begin to discuss the enhancements via new semantics.

First and foremost, let us analyze one of the previously mentioned lambda-terms that we would like in our new framework :

$\lambda \alpha$ : $*$ . $\alpha \to \alpha$

We would like this term can be a placeholder for any Type that is a binary operation of the arrow on itself. Therefore, we would like to type the term as :

$\lambda \alpha$ : $*$ . $\alpha \to \alpha$ : $*\to *$ In order to be able to generically type these "higher-order" Types, we need a new Super-Type to represent $*$ and all $*$ expressions over the binary operator $\to$. Terms from the said set are generally typed as : $\square$

So, all types like : $*,*\to *,(*\to *)\to *,...$ have type : $\square$

Furthermore, to formalize this notion of abstract structure over these "higher-types", we introduce some simple terminology and grammar :

$𝕂$ = $*$ $|$ $𝕂\to 𝕂$

It is easy to see (by definition, in fact), that, $\forall \kappa \in 𝕂$, $\kappa :\square$.

These abstract "higher-types" are termed Kinds. They represent the Set of the new, more powerful Types that we want to type terms with and substitute into (in ${\lambda }_{\omega }$).

The types : $*,\square$ have a special name - sorts. They are represented as : sorts = {$*,\square$}. The symbol $s$ refers to $*$ or $\square$.

Terms such as the ones defined above, that take Types and construct new terms (of Types) from them, are called Type-Constructors.

Formally :

A Type-Constructor is a term $M\in {\Lambda }_{\omega }$, $\ni$, $M:\kappa$.

If $\kappa \ne *$, then it is referred to as a Proper Type-Constructor.

Now that we have an idea of what we want our Lambda-Terms in ${\lambda }_{\omega }$ to look like, and what exactly our "Higher-Types" must look like, we can begin to introduce the Rules and Formal Semantics of our system.

The first thing we need to do is introduce the "Super-Type" $\square$ in our Derivation rules so as to construct complex types. This is done via the $\left(sort\right)$ rule :

$\left(sort\right)$ $\varphi$ $⊢*:\square$

This rule is necessary for 2 reasons :

a) It allows us to introduce $*$ and generically typed type-variables

b) It lays the foundations for the usage of the $\left(form\right)$ rule (introduced ahead) on empty contexts ($\Gamma \equiv \varphi$)

Now that we can introduce the super-type ($\square$) into our Lambda-Calculus, the next thing we want is the ability to introduce variables at 2 levels :

a) Those with type $*$

b) And variables that have a type of a type-variable

This is achieved via the $\left(var\right)$ rule :

As $s$ represents a term from the set : $\{*,\square \}$ we can see that 2 levels of terms can be introduced here. As an example, consider the following :

However, with just $\left(sort\right)$ and $\left(var\right)$ we can’t generate all things that are present in the context ($\Gamma$). As an example, the following generations are not possible :

$\alpha$ : $*,\beta$ : $*⊢\beta$ : $*$

$\alpha$ : $*,\beta$ : $*⊢\alpha$ : $*$

We need to solve this issue by effectively allowing for the weakening of $\Gamma$ by allowing us to "re-derive" $*$ : $\square$ no matter what exactly $\Gamma$ is. The rule that introduces this into the semantics of ${\lambda }_{\omega }$ is $\left(weak\right)$ :

Again, it’s easy to see that the Rule allows for "weakening" at the level of terms of types, and types of higher-kinds. This can be seen pretty easily in the following example :

So, we’ve gained the ability to fully express our Context ($\Gamma$) and introduce the super-type into our derivations. The only semantic we need before introducing $\left(appl\right)$ and $\left(abst\right)$ into our rules is that of the ability to construct any $\kappa \in 𝕂$. This can be introduced by the simple $\left(form\right)$ rule :

Once again, it is easy to see that this not only introduces the elements of $𝕂$, but also allows us to type term-variables with type-variables.

We are now in a place to introduce the much awaited $\left(appl\right)$ and $\left(abst\right)$ rules for ${\lambda }_{\omega }$ :

These rules are actually fairly intuitive, and once again, easy to verify as to being applicable for introducing and applying to term-variables and type-variables.

The last rule that we need to construct our Types-Depdent-On-Types ${\lambda }_{\omega }$ is the $\left(conv\right)$ rule :

The reason we need the $\left(conv\right)$ rule is to formalize our intuition for circumstances where a variable can be typed with 2 $\beta$-equivalent types. Consider the following type-term :

$(\lambda \alpha$ : $*$ . $\alpha$ . $\alpha \to \alpha )\beta$ ${\to }_{\beta }$ $\beta \to \beta$

Supposing we have some $\Gamma$, where, $x$ : $(\lambda \alpha$ : $*$ . $\alpha$ . $\alpha \to \alpha )\beta$ and $x\in \Gamma$

Clearly, $x$ : $\beta \to \beta$ as a type is equivalent to the one that $x$ is typed with in the context $\Gamma$. This is the exact intuition that the $\left(conv\right)$ rule formalizes. The $\left(conv\right)$ rule allows this for all types up to $\beta$-equivalence.

One should be careful so as to not confuse the Subject-Reduction Lemma with the $\left(conv\right)$ rule. The former states that two $\beta$-equivalent terms have the same type, while the latter states that a term can be typed with all $\beta$-equivalent types. If there is some confusion regarding the fact that $\beta$-reduction is applying over here to terms and types, then one can simply glance at the rules for ${\lambda }_{\omega }$ to understand that, as types are more complicated in ${\lambda }_{\omega }$ and can be applied to and abstracted on to create more types, type-variables can be manipulated in ways that they can’t in $\lambda 2$. Hence, the concept of Dependent-Types.

Having derived all the Formal Semantics of ${\lambda }_{\omega }$ we can now rewrite them collectively, and move on to the important Properties :

This is it. This is the ${\lambda }_{\omega }$.

As a last note - The ${\lambda }_{\omega }$ does not contain $\prod$-types. However, Girard’s extension of ${\lambda }_{\omega }$ into what is called "System $F_{\omega }$" does.

PROPERTIES : This section is going to be succinct and I will mention the 3 most important properties about ${\lambda }_{\omega }$ :

Theorem 1 : Uniqueness of Types - $\forall A\in {\Lambda }_{\omega }$, if, $(\Gamma ⊢A$ : $B_1)\wedge (\Gamma ⊢A$ : $B_2)$, then, $B_1{=}_{\beta }{B}_2$.

This Lemma is basically stating a formalism of the fact that a term can only be typed by two types if they are equivalent. The proof for this follows from Induction on the ways a term $M\in {\Lambda }_{\omega }$ can be built, and using the $\left(conv\right)$ rule for the Inductive Hypothesis.

Theorem 2 : Church-Rosser Theorem - $\forall M,N_1,N_2\in {\Lambda }_{\omega }$, $\ni$ $\left(M{\to }_{\beta }{N}_1\right)\wedge \left(M{\to }_{\beta }{N}_2\right)$, $\exists$ $N\in {\Lambda }_{\omega }$, $\ni$ $M{\to }_{\beta }N$.

For a generic Proof of this Theorem, one may refer to the work by Henk Barendregt or that of Takahashi, 1995. The important part is that the theorem holds for the System ${\lambda }_{\omega }$.

Theorem 3 : Strong Normalization Theorem - $\forall M\in {\Lambda }_{\omega }$, $\exists$ $\pi =M{\to }_{\beta }{M}_1{\to }_{\beta }{M}_2...{\to }_{\beta }{M}_n$, where, $M_n$ is in $\beta$-nf.

This Theorem basically states that every term in ${\lambda }_{\omega }$ is strongly-normalizing, or that evaluating leads to termination (and no form of undecidability or infinite looping). The Proof for this Theorem is highly non-trivial and uses the concept of Logical Relations to find a property that is an inductive invariant for the System.

At this point, we have covered a lot of ground and laid the foundations for ${\lambda }_{\omega }$ by stating the motivating behind its construction, its semantics, and its three most crucial properties.

So, until the next post (where we will cover the Calculus-of-Constructions), the reader is encouraged to prove the 3 Properties!