In type theory, a typing 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 typing rules is in defining type inference in the simply typed lambda calculus, which is the internal language of Cartesian closed categories.
Notation Typing rules specify the structure of a typing relation that relates syntactic terms to their types. Syntactically, the typing relation is usually denoted by a colon, so for example e : τ {\displaystyle e:\tau } denotes that an expression e {\displaystyle e} has type τ {\displaystyle \tau } . The rules themselves are usually specified using the notation of natural deduction. For example, the following typing rules specify the typing relation for a simple language of booleans:
t r u e : B o o l f a l s e : B o o l e 1 : B o o l e 2 : τ e 3 : τ i f e 1 t h e n e 2 e l s e e 3 : τ {\displaystyle {\frac {}{{\mathsf {true}}:{\mathsf {Bool}}}}\qquad {\frac {}{{\mathsf {false}}:{\mathsf {Bool}}}}\qquad {\frac {e_{1}:{\mathsf {Bool}}\quad \;e_{2}:\tau \quad \;e_{3}:\tau }{\mathbf {if} \ e_{1}\ \mathbf {then} \ e_{2}\ \mathbf {else} \ e_{3}:\tau }}}
Each rule states that the conclusion below the line may be derived from the premises above the line. The first two rules have no premises above the line, so they are axioms. The third rule has premises above the line (specifically, three premises), so it is an inference rule. In programming languages, the type of a variable depends on where it is bound, which necessitates context-sensitive typing rules. These rules are given by a typing judgment, usually written Γ ⊢ e : τ {\displaystyle \Gamma \vdash e:\tau } , which states that an expression e {\displaystyle e} has type τ {\displaystyle \tau } under a typing context Γ {\displaystyle \Gamma } that relates variables to their types. Typing contexts are occasionally supplemented by the types of individual variables; for example, Γ , x : τ 1 ⊢ e : τ 2 {\displaystyle \Gamma ,x{:}\tau _{1}\vdash e:\tau _{2}} can be read as "the context Γ {\displaystyle \Gamma } supplemented by the information that the expression x {\displaystyle x} has type τ 1 {\displaystyle \tau _{1}} yields the judgement that expression e {\displaystyle e} has type τ 2 {\displaystyle \tau _{2}} ". This notation can be used to give typing rules for variable references and lambda abstraction in the simply typed lambda calculus:
… excerpt ends here. Continue reading the full article.
