4
$\begingroup$

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)?

Improve this question
$\endgroup$
2
  • 2
    $\begingroup$ Instead of "context $\Gamma$ containing $x$ of type $\tau_1$" you should say "context $\Gamma$ extended with $x$ of type $\tau_1$". It is assumed here that $\Gamma$ itself does not contain $x$. Thus, below the line, where the context is $\Gamma$, the variable $x$ is "not known". $\endgroup$
    – Andrej Bauer
    Commented Jul 24, 2014 at 15:15
  • $\begingroup$ A related question and answer on StackOverflow: “What part of Milner-Hindley do you not understand?”. Comes with in‑deep explanations on the notations meaning. $\endgroup$
    – Hibou57
    Commented Jul 26, 2014 at 1:09

1 Answer 1

Reset to default
5
$\begingroup$

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.

Improve this answer
$\endgroup$
15
  • $\begingroup$ “By writing Γ,x:τ 1, we are considering a context Γ where the variable x has type τ1, ignoring what the type of x may have been in context Γ alone.”: so in short there is a difference between Γ added x, and x is part of Γ. $\endgroup$
    – Hibou57
    Commented Jul 24, 2014 at 13:07
  • 1
    $\begingroup$ @Hibou57 I am not sure what you mean by "Γ added x", and by "x is part of Γ". All I am saying is that explicit type assigment to the variable x will supersede any that may be (if any) already in Γ. This is actually how shadowing of variables operates, regarding typing (shadowing is also called scope hole in programming languages). At least I believe that is what is intended in your document. I do not recall using the word "shadowing" for that phenomenon. $\endgroup$
    – babou
    Commented Jul 24, 2014 at 13:31
  • $\begingroup$ I meant “temporarily or locally added”, you say shadowing, which is clearer. Don't mind, your answer was clear to me and will probably be for others. $\endgroup$
    – Hibou57
    Commented Jul 24, 2014 at 13:55
  • 1
    $\begingroup$ @Hibou57 There are often many ways to look at definitions (or to avoid having to look at them, as with De Bruijn index, in more advanced work on these issues). My own inclination is to see Γ as a substitution, i.e. a mapping from variables to types. So if you define Γ' as Γ,x:τ, then Γ' is a mapping identical to Γ, except for the argument x for which it gives the type τ. So you have Γ'(x)=τ, which is a property of Γ', not a notation to define it. But you can say nothing of Γ(x), which may even be undefined. $\endgroup$
    – babou
    Commented Jul 26, 2014 at 15:25
  • 1
    $\begingroup$ @Hibou57 Then the notation x:τ∈Γ is a statement equivalent to Γ(x)=τ, but it is not a definition of anything. And in the context of your question, it is wrong as Γ may not even be defined for the variable x. - - - Writing Γ∪{x:τ} is clearly wrong, as a homonymous bound variable x may already be associated in Γ with another type, thus causing ambiguity. The closest which would make sense would be to see Γ as an ordered list of pairs, with new pairs on the right end, and searched from right to left to find the type of a variable. This is used when implementing contexts. $\endgroup$
    – babou
    Commented Jul 26, 2014 at 17:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.