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

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?

• The OP is asking a lot of questions that are very closely related. Is there a better way to do this? For instance, here we have a question which is conceptually exactly the same as this question. It looks like the OP is reading TAPL and using us to explain things that aren't clear. – Andrej Bauer Oct 7 '16 at 7:35
• Admiteddly, the other question is not from OP, but he should have looked around before asking. – Andrej Bauer Oct 7 '16 at 7:47
• @AndrejBauer "...using us to explain things that aren't clear", isn't allowed or wrong thing to do? – alim Oct 7 '16 at 7:56
• Well, of course, it's kind of the purpose of this site, but I am just wondering what happens when you ask a series of questions that are going to wear out the people who are answering. I am happy to answer questions about type theory, but less so when it is series of questions from the same person that come in quick succession, because then it feels like a personal service. – Andrej Bauer Oct 7 '16 at 15:10
• @AndrejBauer. I see your point. Yes, I am working on that book, solved some issues myself and too confused with others. While asking questions, I felt many people understand theory and when comes to practice quite different story. Actually, I was hoping to get answer to just one of my questions, but did not get much beyond theory. That is why I put several questions. But still, answers cleared my mind a bit. – alim Oct 7 '16 at 16:41

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.

• My title is not suitable, i agree with your recommendation. is there such algorithm ? I searched internet, there is type checking algorithms for let -polymorphic, but did not see any algorithm for type checking for polymorphic lambda calculus. – alim Oct 7 '16 at 8:00

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.