Type rule
In type theory, a type rule is an inference rule that describes how a type system assigns a type to a syntactic construction. These rules may be applied by the type system to determine if a program is well typed and what type expressions have. A prototypical example of the use of type rules is in defining type inference in the simply typed lambda calculus, which is the internal language of Cartesian closed categories.
Notation
An expression [math]\displaystyle{ e }[/math] of type [math]\displaystyle{ \tau }[/math] is written as [math]\displaystyle{ e\!:\!\tau }[/math]. The typing environment is written as [math]\displaystyle{ \Gamma }[/math]. The notation for inference is the usual one for sequents and inference rules, and has the following general form
- [math]\displaystyle{ \frac{\Gamma_1 \vdash e_1\!:\!\tau_1 \quad \cdots \quad \Gamma_n \vdash e_n\!:\!\tau_n}{\Gamma \vdash e\!:\!\tau} }[/math]
The sequents above the line are the premises that must be fulfilled for the rule to be applied, yielding the conclusion: the sequents below the line. This can be read as: if expression [math]\displaystyle{ e_i }[/math] has type [math]\displaystyle{ \tau_i }[/math] in environment [math]\displaystyle{ \Gamma_i }[/math], for all [math]\displaystyle{ i=1..n }[/math], then the expression [math]\displaystyle{ e }[/math] will have an environment [math]\displaystyle{ \Gamma }[/math] and type [math]\displaystyle{ \tau }[/math].
For example, a simple language to perform arithmetic calculations on real numbers may have the following rules
- [math]\displaystyle{ \frac{\Gamma \vdash e_1\!:\!real \quad \Gamma \vdash e_2\!:\!real}{\Gamma \vdash e_1+e_2\!:\!real} \qquad \frac{\Gamma \vdash e_1\!:\!integer \quad \Gamma \vdash e_2 : integer}{\Gamma \vdash e_1+e_2\!:\!integer} \qquad \cdots }[/math]
A type rule may have no premises, and usually the line is omitted in these cases. A type rule may also change an environment by adding new variables to a previous environment; for example, a declaration may have the following type rule, where a new variable [math]\displaystyle{ id }[/math], with type [math]\displaystyle{ \tau' }[/math], is added to [math]\displaystyle{ \Gamma }[/math]:
- [math]\displaystyle{ \frac{\Gamma \vdash e'\!:\!\tau' \quad \Gamma, id\!:\!\tau' \vdash e\!:\!\tau}{\Gamma \vdash \text{let id = } e' \text{ in } e \text{ end} :\!\tau} }[/math]
Here the syntax of the let expression is that of Standard ML. Thus type rules can be used to derive the types of composed expressions, much like in natural deduction.
See also
Further reading
- Cardelli, Luca (March 1996). "Type Systems". ACM Computing Surveys 28 (1): 263–264. doi:10.1145/234313.234418. http://www.cs.colorado.edu/~bec/courses/csci5535/reading/cardelli-typesystems.pdf.
 |
