5
$\begingroup$

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.

enter image description here enter image description here

$\endgroup$
13
$\begingroup$

$\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.

$\endgroup$
1
  • 9
    $\begingroup$ One of the authors of the paper/tutorial here. I can confirm that this is the right answer. $\endgroup$ – kosmikus Jul 13 '20 at 6:21
2
$\begingroup$

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 } } $$

$\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.