patternMinor
Meaning of type inference rule for abstraction in lambda-calculus
Viewed 0 times
meaningrulecalculusabstractioninferencetypeforlambda
Problem
Below is a snippet about simply typed lambda-calculus from CS152: Programming Languages Lecture 9 | Simply Typed Lambda Calculus, on printed‑page 15, indexed 23.
$$
\frac {\Gamma, x: \tau_1 \vdash e: \tau_2}{\Gamma \vdash \lambda x. e: \tau_1 \rightarrow \tau_2}
$$
I read it as: if from a context $\Gamma$ containing $x$ of type $\tau_1$, follows that an expression $e$ is of type $\tau_2$, then from context $\Gamma$, follows that $\lambda x. e$ is of type $\tau_1 \rightarrow \tau_2$.
How does that differs from this:
$$
\frac {\Gamma \vdash x: \tau_1 \land \Gamma \vdash e: \tau_2}{\Gamma \vdash \lambda x. e : \tau_1 \rightarrow \tau_2}
$$
I understand $x$ is expected to typically appears in $e$ (but need not to), however still not see why the second expression (looking more intuitive to me) is not used instead, and so I suspect I may be not really understanding the notation in the first expression.
Is this the same or is this different? If it is not the same, what's the precise meaning of the former and what's the (different) meaning (if it has one) of the latter? Is the former just a way to underline $x$ may be contained in $e$ (i.e., more matter of style than formal meaning)?
$$
\frac {\Gamma, x: \tau_1 \vdash e: \tau_2}{\Gamma \vdash \lambda x. e: \tau_1 \rightarrow \tau_2}
$$
I read it as: if from a context $\Gamma$ containing $x$ of type $\tau_1$, follows that an expression $e$ is of type $\tau_2$, then from context $\Gamma$, follows that $\lambda x. e$ is of type $\tau_1 \rightarrow \tau_2$.
How does that differs from this:
$$
\frac {\Gamma \vdash x: \tau_1 \land \Gamma \vdash e: \tau_2}{\Gamma \vdash \lambda x. e : \tau_1 \rightarrow \tau_2}
$$
I understand $x$ is expected to typically appears in $e$ (but need not to), however still not see why the second expression (looking more intuitive to me) is not used instead, and so I suspect I may be not really understanding the notation in the first expression.
Is this the same or is this different? If it is not the same, what's the precise meaning of the former and what's the (different) meaning (if it has one) of the latter? Is the former just a way to underline $x$ may be contained in $e$ (i.e., more matter of style than formal meaning)?
Solution
The problem is that whatever the context $\Gamma$ may imply about the
variable $x$ is irrelevant. This rule is intended to type a
$\lambda$-abstraction, and the variable $x$ may be changed to another
variable by $\alpha$-conversion, without changing the semantics of the
$\lambda$-abstraction, and thus without changing its type.
By writing $\Gamma, x: \tau_1$, we are considering a context $\Gamma$
where the variable $x$ has type $\tau_1$, ignoring what the type of
$x$ may have been in context $\Gamma$ alone. If $x$ could be assigned
a type in the context $\Gamma$ alone, it would refer to some homonymous variable that is irrelevant to the abstraction, since its scope is shadowed in the abstraction by the local variable $x$. Indeed, an $\alpha$-conversion would make $x$ disappear from $e$ altogether.
In other words: $\Gamma \vdash x: \tau_1$ may or may not be true, but
it is simply irrelevant to typing the abstraction.
Then, it is possible that $\Gamma \vdash e: \tau_2$. But that is only
possible if the type of $x$ is irrelevant, for example when $x$ does
not actually occurs in $e$, as for the abstarction $\lambda x.42$,
Then $e=42$ which is indeed typable. But in general, you cannot type $e$ without having a type for $x$ (for the variable $x$ of the abstraction).
In other words, you expect the type of $e$ to be in general related to the type of $x$, and it is their relation that the rule is intended to express.
What the rule says is that, if by adding to the context $\Gamma$ that the new
variable $x$ has type $\tau_1$, you can infer then that $e$ has type
$\tau_2$ in this new environment, then the abstraction $\lambda x. e$
has type $\tau_1 \rightarrow \tau_2$ in the original environment
$\Gamma$.
It says that the type of $e$ is dependent on the type $x$ may have.
Then, wherever the abstraction is applied to another expression $e'$, the type of the application is whathever the type of $e$ should be when the type of $x$ is that of $e'$. But that is another typing rule.
variable $x$ is irrelevant. This rule is intended to type a
$\lambda$-abstraction, and the variable $x$ may be changed to another
variable by $\alpha$-conversion, without changing the semantics of the
$\lambda$-abstraction, and thus without changing its type.
By writing $\Gamma, x: \tau_1$, we are considering a context $\Gamma$
where the variable $x$ has type $\tau_1$, ignoring what the type of
$x$ may have been in context $\Gamma$ alone. If $x$ could be assigned
a type in the context $\Gamma$ alone, it would refer to some homonymous variable that is irrelevant to the abstraction, since its scope is shadowed in the abstraction by the local variable $x$. Indeed, an $\alpha$-conversion would make $x$ disappear from $e$ altogether.
In other words: $\Gamma \vdash x: \tau_1$ may or may not be true, but
it is simply irrelevant to typing the abstraction.
Then, it is possible that $\Gamma \vdash e: \tau_2$. But that is only
possible if the type of $x$ is irrelevant, for example when $x$ does
not actually occurs in $e$, as for the abstarction $\lambda x.42$,
Then $e=42$ which is indeed typable. But in general, you cannot type $e$ without having a type for $x$ (for the variable $x$ of the abstraction).
In other words, you expect the type of $e$ to be in general related to the type of $x$, and it is their relation that the rule is intended to express.
What the rule says is that, if by adding to the context $\Gamma$ that the new
variable $x$ has type $\tau_1$, you can infer then that $e$ has type
$\tau_2$ in this new environment, then the abstraction $\lambda x. e$
has type $\tau_1 \rightarrow \tau_2$ in the original environment
$\Gamma$.
It says that the type of $e$ is dependent on the type $x$ may have.
Then, wherever the abstraction is applied to another expression $e'$, the type of the application is whathever the type of $e$ should be when the type of $x$ is that of $e'$. But that is another typing rule.
Context
StackExchange Computer Science Q#28682, answer score: 5
Revisions (0)
No revisions yet.