I realized that almost no one explained how to selected the type variable T1

 Γ ⊢ e1 : T1 -> T  ,  Γ ⊢ e2 : T1
 -------------------------------- T-APP 
 Γ ⊢ e1 e2 : T

when doing type checking (from bottom to top).

So, the question is how T1 is introduced? Is there any condition about T1?


T1 is a schematic variable. Every consistent substitution of T1 with a type produces an instance of the rule. In a simple enough system, the inference rules can be used directly as the blueprint for a type-checking algorithm. In languages with richer type systems, type-checking algorithms become more complex or even undecidable (which is not a desirable features). Let me give an example where I type-check the program using a simple derivation.

Let's say I have the following program I wish to type-check:

(lambda x: nat. x = 0)(4)

First, we can deduce that 4 : nat by using the usual typing rules for natural numbers, which I will not reproduce here. Then we type-check the lambda abstraction with following derivation (I apologize for the sloppy latex):

$$ \underline{x : nat ⊢ x: nat \quad x: nat ⊢ 0 : nat} $$ $$ \underline{x : nat ⊢ x = 0 : bool}$$ $$ \underline{\lambda x: nat. \ x = 0 : nat \to bool} $$

Finally, using the application rules:

$$ \underline{\lambda x: nat. \ x = 0 : nat \to bool \quad 4 : nat} $$ $$ (\lambda x: nat. \ x = 0)(4) : bool $$

Note that type-checking is much simpler when we're working in a type system without subtyping, in that ever expression is monomorphic. The typing rules are syntax-directed. That is, the structure of the program dictates the type of every expression.

  • $\begingroup$ It would be great if you could make your derivation look standard(with horizontal lines), I am having difficulty on reading it. $\endgroup$
    – alim
    Oct 2 '16 at 17:22

It depends on what the expression e2 (and e1) is and what other type rules are in the type system.

Basically, the Γ ⊢ e2 : T1 part of the type rule says:

If there is a rule in the type system, which assigns the type T1 to the expression e2 in the environment Γ

If you can also find a rule that assigns the type T1 -> T to e1, then you can use the type assignment from the conclusion.

  • $\begingroup$ You are right in practice, but this kind of judgments doesn't specify how you actually type check a program. They're done top-down. If you want to see a better formalization of how type checking works, check out "bidirectional type checking". $\endgroup$
    – 盛安安
    Oct 2 '16 at 19:00
  • 3
    $\begingroup$ Typing rules are not algorithms. They tell you what is allowed, but not what to do. $\endgroup$ Oct 2 '16 at 19:28
  • $\begingroup$ still, I did not understand how do we know what T1 is at the moment when we are applying T-APP rule. $\endgroup$
    – alim
    Oct 3 '16 at 7:14

"T1" is obtained from typing context by doing derivation on the right branch of application rule. I worked on some type checking examples and concluded that.


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.