I started reading more and more language research papers. I find it very interesting and a good way to learn more about programming in general. However, there usually comes a section where I always struggle with (take for instance part three of this) since I lack the theoretical background in computer science: Type Rules.
Are there any good books or online resources available to get started in this area? Wikipedia is incredibly vague and doesn't really help a beginner.
In most type systems, the type rules work together to define judgements of the form:
$$\Gamma\vdash e:\tau$$
This states that in context $\Gamma$ the expression $e$ has type $\tau$.
$\Gamma$ is a mapping of the free variables of $e$ to their types.
A type system will consist of a set of axioms and rules (a formal system of rules of inference, as Raphael points out).
An axiom is of the form
$$\dfrac{}{\Gamma \vdash e:\tau}$$
This states that the judgement $\Gamma \vdash e:\tau$ holds (always).
An example is
$$\dfrac{}{x:\tau\vdash x:\tau}$$
which states that under the assumption that the type of variable $x$ is $\tau$, then the expression $x$ has type $\tau$.
Inference rules take facts that have already been determined and build larger facts from them. For instance the inference rule
$$\dfrac{\Gamma\vdash e_1:\tau\to\tau' \quad \Gamma\vdash e_2:\tau}{\Gamma\vdash e_1\ e_2:\tau'}$$
says that if I have a derivation of the fact $\Gamma\vdash e_1:\tau\to\tau'$ and a derivation of the fact $\Gamma\vdash e_2:\tau$, then I can obtain a derivation of the fact $\Gamma\vdash e_1\ e_2:\tau'$. In this case, this is the rule for typing function application.
There are two ways of reading this rule:
Some inference rules also manipulate $\Gamma$ by adding new ingredients into it (view-ed bottom up). Here is the rule for $\lambda$-abstraction:
$$\dfrac{\Gamma x:\tau\vdash e:\tau'}{\Gamma\vdash \lambda x.e:\tau\to \tau'}$$
The inference rules are applied inductively based on the syntax of the expression being considered to form a derivation tree. At the leaves of the tree (at the top) will be axioms, and branches will be formed by applying inference rules. At the very bottom of the tree is the expression you are interested in typing.
For example, a derivation of the typing of expression $\lambda f.\lambda x.f\ x$ is
$$\dfrac{\dfrac{}{f:\tau\to\tau',x:\tau\vdash f:\tau\to\tau'} \qquad \dfrac{}{f:\tau\to\tau',x:\tau\vdash x:\tau}} {\dfrac{f:\tau\to\tau',x:\tau\vdash f\ x:\tau'}{ \dfrac{f:\tau\to\tau'\vdash \lambda x.f\ x:\tau'}{\vdash \lambda f.\lambda x.f\ x:\tau'}}}$$ Two very good books for learning about type systems are:
Both books are very comprehensive, yet they start slowly, building a solid foundation.
There is cute interactive online tutorial on sequent calculus, which may help to build some intuitions and to feel how inference works: An Interactive Tutorial of the Sequent Calculus
In that Wikipedia page it is recommended "Type Systems, Luca Cardelli, ACM Computing Surveys", which is a 2-pages survey that can help you to understand how to read a rule. Anyway, how to read a rule is perfectly explained in that Wikipedia page (or even better in the 2-pages survey). However to understand the whole thing, you need to understand what is a typing system (composed by several rules), for which the "Type system" Wikipedia article is a good start (and you have several books in the section "References" of that page if you want to go further).
