patternMinor
Understanding the Reasoning Behind These Typing Rules
Viewed 0 times
reasoningunderstandingthethesetypingbehindrules
Problem
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
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 u
\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 u
Solution
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.
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.
Context
StackExchange Computer Science Q#92701, answer score: 6
Revisions (0)
No revisions yet.