Typing rule

In type theory and programming language theory, a typing rule is an inference rule that specifies sufficient conditions for a typing judgment to hold. A common form of typing judgment is

${\displaystyle \Gamma \vdash e:\tau ,}$

read as “under typing context ${\displaystyle \Gamma }$, expression ${\displaystyle e}$ has type ${\displaystyle \tau }$”. A collection of typing rules normally defines a typing relation inductively: a judgment holds when it has a finite derivation constructed from the rules. A program is well-typed when its required top-level typing judgment can be derived.

Typing rules are relational specifications rather than necessarily functions from expressions to types. Depending on the type system, an expression may have no derivable type, one type, or several types. Rules may be presented as a declarative mathematical specification or organized into a procedure for type checking or type inference. A common algorithmic organization is bidirectional typing, which distinguishes rules that synthesize a type from rules that check an expression against a type already known from its context.