Question on the “Tutorial implementation of dependently typed lambda calculus”

Question

I have a slight technical struggle with this marvelous tutorial. On page 5 the tutorial talks about typing rules for Simply Typed Lambdas and presents following judgement as derivable via rules on figure 3.

I was unable to prove neither id nor const by the same reason. Take for instance the id example.

• Say I am looking on type checking rule CHK. It says that in order to check types I should first perform inference and then compare result with what I expect.
• To do the inference on application, I have to use the APP rule that immediately forces me to infer the type of the left hand side of the application, namely (id :: α -> α)
• To do that I am using the ANN rule that forces me to check that α -> α is a type (and I can prove it no problem). Then I got this naked id symbol and have to prove it's type to be α -> α.
• Finally, here is a problem. In order to do that I will have to use var rule, which requires the type of id to be set in the context Gamma explicitly, but it is not done, therefore the proof is falling apart.

Answer 1

$\mathsf{id}$ and $\mathsf{const}$ are not variables of the calculus, but syntactic sugar for $\lambda x \rightarrow x$ and $\lambda x \rightarrow \lambda y \rightarrow x$ respectively. This is stated at the end of §2.2 and subtly conveyed by the use of a sans-serif font rather than italics (this is a typographic convention of this particular document, not a common convention).

So for example the type judgement $$ \alpha :: \ast, y :: \alpha \vdash (\mathsf{id} :: \alpha \rightarrow \alpha) \: y :: \rightarrow \alpha $$ is also the type judgement $$ \alpha :: \ast, y :: \alpha \vdash (\lambda x \rightarrow x :: \alpha \rightarrow \alpha) \: y :: \rightarrow \alpha . $$ It's a different notation for the same mathematical object.

Answer 2

As an example, here is the full derivation for the type judgement $$\alpha::\ast,y::\alpha \vdash (\lambda x \rightarrow x :: \alpha \rightarrow \alpha) \: y :: \alpha$$ where $\enspace \Gamma = \alpha::\ast,y::\alpha \enspace$ and $\enspace \Gamma' = \Gamma,x::\alpha \enspace$:

$$ { \dfrac { \dfrac { \Gamma \vdash \alpha \rightarrow \alpha :: \ast \qquad \dfrac { \dfrac { \dfrac { \Gamma'(x)=\alpha } { \Gamma,x :: \alpha \vdash x ::_\uparrow \alpha } { \tiny VAR } } { \Gamma,x :: \alpha \vdash x ::_\downarrow \alpha } { \tiny CHK } } { \Gamma \vdash \lambda x \rightarrow x ::_\downarrow \alpha \rightarrow \alpha } { \tiny LAM } } { \Gamma \vdash (\lambda x \rightarrow x :: \alpha \rightarrow \alpha) ::_\uparrow \alpha \rightarrow \alpha } { \tiny ANN } \qquad \dfrac { \dfrac { \Gamma(y) = \alpha } { \Gamma \vdash y ::_\uparrow \alpha } { \tiny VAR } } { \Gamma \vdash y ::_\downarrow \alpha } { \tiny CHK } } { \dfrac { \Gamma \vdash (\lambda x \rightarrow x :: \alpha \rightarrow \alpha)\ y ::_\uparrow \alpha } { \Gamma \vdash (\lambda x \rightarrow x :: \alpha \rightarrow \alpha)\ y ::_\downarrow \alpha } { \tiny CHK } } { \tiny APP } } $$