3
$\begingroup$

What is a Context? Is it like a scope in C? Does it have a start and an end? Can contexts contain other contexts?

I see Contexts being used in lambda calculi type system rules, but I don't understand concretely what they are and why they are necessary. If they are too abstract, then is there some visual or metaphorical description?

Update: I am referring to "contexts" as what is to the left of ⊢ in typing calculi.

$\endgroup$
2
  • $\begingroup$ A context is just a dictionary/hashmap/association-list consisting of name-type pairs: Given a name, if it is in the context, then it is associated a type. That is all ^_^ In some sense, this is the notion of scope in C ;-) $\endgroup$ – Musa Al-hassy Apr 26 '20 at 9:07
  • 1
    $\begingroup$ Do you mean contexts as in what's to the left of $\vdash$ in typed calculi (which is what the current answer and comment are about), or contexts as in $[]$ in reduction rules (with or without types)? They are different concepts. $\endgroup$ – Gilles 'SO- stop being evil' Apr 26 '20 at 11:50
1
$\begingroup$

Typing contexts are the way to remember previously declared variables when type-checking a program/term. The rule for term abstraction usually is something like $$\dfrac{\Gamma,x:A\vdash e : B}{\Gamma\vdash \lambda x.e : A\to B}$$ In the conclusion, $x$ is not in $\Gamma$ yet. At this point, $x$ is declared to be the variable of the function $\lambda x.e$ and this variable appears in $e$. So, $x$ is a free variable in $e$. The typing rule above expresses that $\lambda x.e$ is of type $A\to B$ under context $\Gamma$ iff $e$ is of type $B$ under context $\Gamma,x:A$. So in the premise of the rule, we are type-checking the body of $\lambda x.e$ (which is $e$), but we need to remember that $x$ (which appears free in $e$) is a variable of type $A$.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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