how to use type application rule (T-TAPP)?

Question

In the following rule,

$$\dfrac{ \Gamma \vdash t_1 : \forall X.T_{12} } { \Gamma \vdash t_1 \ [T_2] : [X \mapsto T_2]T_{12} } \textsf{ (T-TApp)}$$

whend doing type checking, how do know what is $X$?

Also, type checking will not give you a term which has a form $[X \mapsto T_2]T_{12}$, so how to deal with that substitution?

We will have $t_1 \ [T_2]$ during type checking and $T_2$ could be any type such as $T, T \to T,\forall X.T$. How do we know $[X \mapsto T_2]$, again?

I just could not understand how to apply this rule during type checking?

Please help!

Answer 1

Type checking and the inference rules for type theory are not an algorithm. They do not tell you how to type check. They tell you what is allowed when you perform type checking.

The rule for application should be read as:

If you can prove $\Gamma \vdash t_1 : \forall T . T_{12}$ (and we're not telling you how to do that, you'll have to figure it out) then $\Gamma \vdash t_1[T_2] : [X \to T_2]T_{12}$ for whatever $T_2$ you choose to use (and of course we do not know what it is that you're trying to do here, the choice of $T_2$ is entirely up to you).

So, the answer to your question is: you have to figure out how to find the value of $X$ and you have to worry about the subtitution. The rules are not meant to solve that problem. They are just rules, telling you what you may do.

The correct question that you should have asked is: "How do I make an algorithm that will be able to perform type-checking automatically?" This is an important question, and people put a lot of thought into it. I can give you an initial answer: try out all possibilities until you find one that works. But that's a lousy aglorithm and it's possible to do better.

Answer 2

I figured it out. there is a unification needed during type checking.

there is a condition though, $ftv(T_2) \in \Gamma_{tv}$, saying free type variables of $T2$ should be found in the set of type variables in type context.

Also, $X$ could be choose as any new new name which does not clash with existing names.

In type checking, you have $\Gamma \vdash M \quad t_2 : T$, so apply that rule. we can write $\Gamma \vdash M: \forall X.T_1$ where $unify(T , [X \mapsto T_2]T_1$), where $unify(t1,t2)$ check if these two terms are equal.