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
const by the same reason. Take for instance the
- Say I am looking on type checking rule
CHK. It says that in order to
check typesI should first perform inference and then compare result with what I expect.
- To do the inference on application, I have to use the
APPrule 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
ANNrule that forces me to check that
α -> αis a type (and I can prove it no problem). Then I got this naked
idsymbol and have to prove it's type to be
α -> α.
- Finally, here is a problem. In order to do that I will have to use
varrule, which requires the type of
idto be set in the context Gamma explicitly, but it is not done, therefore the proof is falling apart.