1
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ Before we answer the question, can you please tell us how familiar you are with the notion of free vs. bound variables? Can you explain the difference between $x : \mathtt{Nat}, y : \mathtt{Nat} \vdash x + y : \mathtt{Nat}$ and $y : \mathtt{Nat} \vdash \lambda x . (x + y) : \mathtt{Nat} \to \mathtt{Nat}$? $\endgroup$ Sep 6, 2023 at 16:59
  • $\begingroup$ I want to say I'm mostly familiar, in the second example the y within the lambda x is free as it's introduced in the previous abstraction. So if we don't have control over a variable within the current function, it's free, and could be assigned a value at some other point(?) $\endgroup$
    – noCrayCray
    Sep 6, 2023 at 17:27

1 Answer 1

1
$\begingroup$

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?

$\endgroup$
1
  • $\begingroup$ Yes it does, thanks a bunch! We are recording down information about a variable so that we know how to use it later basically, is what I've gathered. I will probably just go over other examples under this light as well. Thanks again! $\endgroup$
    – noCrayCray
    Sep 7, 2023 at 8:38

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.