How to read typing rules?

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.

Answer

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:

  • top-down – given two expressions (a function and another expression) and some constraints on their type, we can construct another expression (the application of the function to the expression) with the given type.
  • bottom-up – given an expression that is, in this case, the application of a function to some expression, the way this is typed is by first typing the two expressions, ensuring that their types satisfy some constraints, namely that the first is a function type and that the second has the argument type of the function.

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.

Attribution
Source : Link , Question Author : suls , Answer Author : gardenhead

Leave a Comment