confused about stlc from Programming Language Foundations

Question

I have two related quetions. I made my way to STLC and Typechecking from Programming Lang Foundations, yet I am more or less mentally stuck at the STLC chapter, hence many things related to it are flying over my head.

Specific question:

In this chapter we are implementing a type checker, we have basic terms and contexts.

  match t with
  | tm_var x =>
      match Gamma x with
      | Some T => return T
      | None   => fail
      end
  | <{ \ x1 : T1, t2 }> =>
      T2 <- type_check (x1 |-> T1 ; Gamma) t2 ;;
      return <{{T1 -> T2}}>
  | <{ t1 t2 }> =>
      T1 <- type_check Gamma t1 ;;
      T2 <- type_check Gamma t2 ;;
      match T1 with
      | <{{T11 -> T12}}> =>
          if eqb_ty T11 T2 then return T12 else fail
      | _ => fail
      end 

as such. I am not sure when to leave the context as plain Gamma and when to add a variable+type binding to it. For example in the function for lists, the given example is

      T0 <- type_check Gamma t0 ;;
      match T0 with
      | <{{List T}}> =>
          T1 <- type_check Gamma t1 ;;
          T2 <- type_check (x21 |-> T ; x22 |-> <{{List T}}> ; Gamma) t2 ;;
          if eqb_ty T1 T2 then return T1 else fail
      | _ => fail
      end

When I defined the sum type, I wrote

 | <{ case t0 of | inl x1 => t1 | inr x2 => t2 }> =>
      T0 <- type_check Gamma t0 ;;
      match T0 with
      |( Ty_Sum T1 T2) =>
          T1' <- type_check Gamma t1 ;;
          T2' <- type_check Gamma t2 ;;
          if (andb (eqb_ty T1 T1') (eqb_ty T2 T2'))
         then return ( Ty_Sum T1 T2) else fail
      | _ => fail
      end

Should I have modified the second Gamma to have t1 |-> T1 , or is this right, or is it all wrong?

Second and vague question: What can I do to understand the coding semantics of this better? I get the whole concept on a theoretical level, I can also mechanically replicate the code I have seen before, but I feel like the intuition isn't there yet.

TIA!

https://softwarefoundations.cis.upenn.edu/plf-current/Typechecking.html

This is the chapter I'm at, and where the code is coming from.

Answer 1

The inference rule for $\lambda$-abstraction is $$ \frac{ \Gamma, x : T_2 \vdash t_2 : T_2 }{ \Gamma \vdash (\lambda x : T_1 .\, t_2) : T_1 \to T_2} $$ Notice how the context changes. Below the line (the conclusion) it is $\Gamma$, above the line it is $\Gamma$ extended with the variable $x$ of type $T_2$. Let us consider a concrete example: $\newcommand{\Nat}{\mathtt{Nat}}$ $$ \frac{ {\displaystyle \frac{y : \Nat, x : \Nat \vdash x : \Nat \qquad y : \Nat, x : \Nat \vdash y : \Nat}{y : \Nat, x : \Nat \vdash x + y : \Nat}}}{ y : \Nat \vdash (\lambda x : \Nat . x + y) : \Nat \to \Nat} $$ In each line the free variables on the right of $\vdash$ are all listed on the left of $\vdash$. This is necessary so that we can tell what each variable is. It would be wrong to write something like $$y : \Nat \vdash x + y : \Nat$$ because $x$ is an "unknown variable". With this in mind, take another look at the top inference rule. If you did not extend $\Gamma$ with $x : T_2$ on the top line, then the variable $x$ would become "unknown".

A good rule of thumb is this: whenever we have a bound variable, say $\lambda x : A . t$ or $\Pi (x : A) . B$ or $\int_0^1 \frac{x}{1 + x^2} dx$, when we check the body of the abstraction, we must extend the context with the variable. For example: $$\frac{\Gamma, x : A \vdash B \ \mathtt{type}}{\Gamma \vdash \Pi (x : A) . B \ \mathtt{type}} $$ and $$ \frac{ \Gamma \vdash 0 : \mathbb{R} \qquad \Gamma \vdash 0 : \mathbb{R} \qquad \Gamma, x : A \vdash \frac{x}{1+x} : \mathbb{R}} {\Gamma : \int_0^1 \frac{x}{1+x} dx : \mathbb{R}} $$ Does this help?