Question on the “Tutorial implementation of dependently typed lambda calculus”
-
29-09-2020 - |
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 tocheck 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 nakedid
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 ofid
to be set in the context Gamma explicitly, but it is not done, therefore the proof is falling apart.
Solution
$\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.