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.