Understanding the Reasoning Behind These Typing Rules

Question

So the expression $\Gamma \ \vdash \ e:\sigma$ states that under assumptions $\Gamma$, the expression $e$ has type $\sigma$. Then we have the following rules:

\begin{array}{cl}\displaystyle {\frac {x:\sigma \in \Gamma }{\Gamma \vdash _{D}x:\sigma }}&[{\mathtt {Var}}]\\\\\displaystyle {\frac {\Gamma \vdash _{D}e_{0}:\tau \rightarrow \tau '\quad \quad \Gamma \vdash _{D}e_{1}:\tau }{\Gamma \vdash _{D}e_{0}\ e_{1}:\tau '}}&[{\mathtt {App}}]\\\\\displaystyle {\frac {\Gamma \vdash _{D}e_{0}:\sigma \quad \quad \Gamma ,\,x:\sigma \vdash _{D}e_{1}:\tau }{\Gamma \vdash _{D}{\mathtt {let}}\ x=e_{0}\ {\mathtt {in}}\ e_{1}:\tau }}&[{\mathtt {Let}}]\end{array}

where

• $\mathtt {Var}$ is variable access.
• $\mathtt {App}$ is function call with one parameter (function application).
• $\mathtt {Let}$ is variable declaration.

I would like to understand how these rules work. This is my understanding so far...

[$\mathtt {Var}$] "if $x$ is of type $\sigma$ from environment $\Gamma$, then under the assumption of $\Gamma$, $x$ is of type $\sigma$." Two things are confusing me so far. First is the $D$ in $\vdash_D$. The second is that the premise and conclusion seem to say the same things: "if x is of type y, then x is of type y". Wondering what this is actually saying so that I can see why it's necessary.

[$\mathtt {App}$] "if under the assumption of $\Gamma$, $e_0$ is of type $\tau \to \tau'$ $\land$ under the assumption of $\Gamma$, $e_1$ is of type $\tau$, then under the assumption of $\Gamma$, $e_0\ e_1$ is of type $\tau$." So that last part is introducing some new syntax $e_0\ e_1$, which means function application. So that makes sense. What I get confused about is the "if, then" part in this definition. Wondering if it is saying, "if the function and the parameter are present, then we can do function application", or "if the function and parameter are present, then function application occurs." I keep on interpreting it as the latter for some reason.

[$\mathtt {Let}$] "if under the assumption of $\Gamma$, $e_0$ is of type $\sigma$, and under the assumption of $\Gamma$ and $x$ of type $\sigma$, $e_1$ is of type $\tau$, then under the assumption of $\Gamma$ we can do $\mathtt {let}\ x=e_{0}\ {\mathtt {in}}\ e_{1}$ of type $\tau$." That "we can do" part is my understanding that this is saying, because of these premises, we can declare a variable. Also I'm not sure about the $\Gamma ,\,x:\sigma\vdash _{D}$, wondering if that is just saying that $x:\sigma$ is in the environment $\Gamma$, or if it's a separate thing. So basically it is just highlighting the fact that we are in the environment and we have this particular type of interest in the environment.

So to summarize, the questions are:

1. The meaning of $D$ in $\vdash_D$.
2. In $\mathtt {Var}$, wondering what the definition is actually saying and why it is necessary.
3. If my understanding of $\mathtt {App}$ and $\mathtt {Let}$ are correct.

Answer 1

For question 1, I don't think that the $D$ carries any particular meaning, it is just part of the notation, and might refer to the name given to the corresponding calculus.

For 2, what you need to understand is that $\Gamma$ really is a set of assumptions. So if $\Gamma = x_1 : \sigma_1, \dots, x_n : \sigma_n$ then $\Gamma$ is a typing context that tells us that we will assume that $x_1$ has type $\sigma_1$, that $x_2$ has type $\sigma_2$ and so on.

Now, what might be confusing to you is that there are several different levels of implications in the syntax of typing rules.

• First, the typing rules themselves are implications of the form "if the premises hold, then the conclusion hold" (the premises being the hypotheses given above the line, and the conclusion being the typing judgment below the line.

• Second, a typing judgments $\Gamma \vdash e : \sigma$ is also a form of implication, meaning "if the assumptions on the types of variables given in $\Gamma$ are correct, then $e$ has type $\sigma$".

• And finally, there is also the arrow type $\sigma_1 \to \sigma_2$, which is also a form of implication.

So in the end, what the [Var] rule says, is that we may assume that $x$ has type $\sigma$, provided that this is part of our assumptions. Or in other words, it is always true that $x$ has type $\sigma$ under the assumption that $x$ has type $\sigma$. Or, reformulating again: when you made an assumption, you have the right to use it.

For 3, the main thing that you need to understand is that typing rules are implications (as explained above). For example, [App] says that if we can show that $e_1$ has an arrow type and that $e_2$ has the same type as the domain of the arrow (i.e., $e_1$ and $e_2$ have compatible types), then we can perform an application.

Answer 2

In addition to the other answer:

In Var, wondering what the definition is actually saying and why it is necessary.

Indeed, the rule might seem trivial, but the point is that by introducing typing judgements we build another layer on top of our syntax, namely a set of assertions that some terms have some types: $\Gamma \vdash e : \tau$.
Therefore, it is natural to have one typing rule for every term in the inductive definition of terms (e.g. $s, t ::== x | \lambda x. s | s t$ for the simply typed Lambda calculus).

Note that terms may have multiple types. Let $\Gamma = \{x: \text{Int}\}$ and $t = x$, then $\Gamma \vdash t: \text{Int}$, $\Gamma \vdash t: \forall \alpha. \text{Int}$ and $\Gamma \vdash t: \forall \alpha, \beta. \text{Int}$ are all equally valid assertions which are inferable.

Hence, you can interpret $\Gamma \vdash t: \sigma$ more like: there is an inference of that type for $t$ or we can deal with $t$ as if it was of type $\sigma$. Especially, you can apply different inferences in different places.

Example: Let $$ \Gamma = \{42: \text{Int}, \text{false}: \text{bool}, \text{toStr}: \forall \alpha. \alpha \rightarrow \text{String}, \text{concat}: \text{String} \rightarrow \text{String} \rightarrow \text{String}\}, $$

then $\Gamma \vdash \text{concat } (\text{toStr } 42)\ (\text{toStr } \text{false}) : \text{String}$ is inferable. On the first occurrence of $\text{toStr}$, its type is inferred as $\text{Int} \to \text{String}$, but upon the second occurrence, it is inferred as $\text{bool} \to \text{String}$.