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.

• It would be great if you could make your derivation look standard(with horizontal lines), I am having difficulty on reading it.
– 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.

• 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".
– 盛安安
Oct 2 '16 at 19:00
• Typing rules are not algorithms. They tell you what is allowed, but not what to do. Oct 2 '16 at 19:28
• still, I did not understand how do we know what T1 is at the moment when we are applying T-APP rule.
– 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.