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

\Gamma \vdash e:\tau ,

read as “under typing context $\Gamma$ , expression $e$ has type $\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.^[1]^: 13–16^[2]^: 91–94 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.^[3]

Judgments, contexts and derivations

The context $\Gamma$ records assumptions needed to type the free variables or other names occurring in an expression. In a simple type system it is often represented as a finite mapping from variables to types:

\Gamma =x_{1}{:}\tau _{1},\ldots ,x_{n}{:}\tau _{n}.

The notation $\Gamma ,x{:}\tau$ means that the context has been extended with the assumption that $x$ has type $\tau$ . A closed expression, having no free variables, is commonly typed under the empty context $\varnothing$ .^[1]^: 35–39

More elaborate systems may use several contexts or auxiliary judgments. These can record type variables, kinds, locations, constraints, effects, modules, or resources. Examples of auxiliary judgments include type formation, type equality, subtyping, and kinding. The structure of a context is also significant: ordinary structural type systems often treat contexts as finite mappings, whereas linear and other substructural systems may make order or multiplicity relevant.

An inference rule is conventionally written

{\frac {J_{1}\qquad \cdots \qquad J_{n}}{J}},

where $J_{1},\ldots ,J_{n}$ are the rule's premises and $J$ is its conclusion. The rule states that the conclusion may be derived whenever all its premises have been derived. A rule with no premises is an axiom. Rules can also contain side conditions, such as a freshness requirement or a membership test on a context.^[1]^: 13–15

Typing rules are generally rule schemes: their metavariables range over all expressions, types, and contexts of the language. A typing derivation is a finite tree whose nodes are judgments, whose root is the judgment being established, and whose children are the premises of the rule used at that node. The inductive structure of derivations is later used in proofs about the type system.

Example: simply typed lambda calculus

Consider a version of the simply typed lambda calculus with booleans. Its types and expressions can be described by the grammars

{\displaystyle \tau

and

e::=x\mid {\mathsf {true}}\mid {\mathsf {false}}\mid \mathbf {if} \ e\ \mathbf {then} \ e\ \mathbf {else} \ e\mid \lambda x{:}\tau .\,e\mid e\ e.

Boolean constants are typed by axiom schemes:

{\frac {}{\Gamma \vdash {\mathsf {true}}:{\mathsf {Bool}}}}\quad {\text{(T-True)}}\qquad {\frac {}{\Gamma \vdash {\mathsf {false}}:{\mathsf {Bool}}}}\quad {\text{(T-False)}}.

A conditional requires a Boolean condition and branches having the same type:

{\frac {\Gamma \vdash e_{1}:{\mathsf {Bool}}\qquad \Gamma \vdash e_{2}:\tau \qquad \Gamma \vdash e_{3}:\tau }{\Gamma \vdash \mathbf {if} \ e_{1}\ \mathbf {then} \ e_{2}\ \mathbf {else} \ e_{3}:\tau }}\quad {\text{(T-If)}}.

Variables, abstractions, and applications are typed by the following rules:

{\frac {x{:}\tau \in \Gamma }{\Gamma \vdash x:\tau }}\quad {\text{(T-Var)}}

{\frac {\Gamma ,x{:}\tau _{1}\vdash e:\tau _{2}}{\Gamma \vdash \lambda x{:}\tau _{1}.\,e:\tau _{1}\mathbin {\to } \tau _{2}}}\quad {\text{(T-Abs)}}

{\frac {\Gamma \vdash e_{1}:\tau _{1}\mathbin {\to } \tau _{2}\qquad \Gamma \vdash e_{2}:\tau _{1}}{\Gamma \vdash e_{1}\,e_{2}:\tau _{2}}}\quad {\text{(T-App)}}.

These rules are schemes because $\Gamma$ , $e$ , and the types may be replaced by arbitrary instances. For example, the rules derive

\varnothing \vdash (\lambda x{:}{\mathsf {Bool}}.\,x)\,{\mathsf {true}}:{\mathsf {Bool}}.

The abstraction rule checks the body under a context extended with an assumption about the bound variable. In its conclusion, that assumption has been abstracted into the function type. In proof-theoretic terms, T-Abs is an introduction rule for the function type and T-App is its elimination rule. This correspondence with the introduction and elimination rules of natural deduction is part of the Curry–Howard correspondence.^[2]^{: 93, 101–103}^[1]^: 35–39

Let binding

A monomorphic let construct can be specified by

{\frac {\Gamma \vdash e_{1}:\tau _{1}\qquad \Gamma ,x{:}\tau _{1}\vdash e_{2}:\tau _{2}}{\Gamma \vdash \mathbf {let} \ x=e_{1}\ \mathbf {in} \ e_{2}:\tau _{2}}}.

Here $x$ is available in $e_{2}$ at the single type $\tau _{1}$ . This is not the full rule for Hindley–Milner let-polymorphism. In a Hindley–Milner system, eligible type variables in the type of $e_{1}$ can be generalized into a type scheme, whose different occurrences may subsequently be instantiated at different types.^[4]

Declarative and algorithmic presentations

A declarative type system characterizes which typing judgments are valid without necessarily prescribing how to find their derivations. A declarative rule may leave some information to be chosen nondeterministically. For example, a subsumption rule in a system with subtyping may be written

{\frac {\Gamma \vdash e:\tau \qquad \tau <:\sigma }{\Gamma \vdash e:\sigma }}\quad {\text{(Sub)}}.

The conclusion does not indicate at which point subsumption should be applied or which intermediate type should be chosen. Similarly, a rule that instantiates a universally quantified type can require a choice of the type used for the instantiation.

A rule system is syntax-directed, relative to a chosen division between inputs and outputs, when the input components of a judgment determine at most one rule that can apply. In a simple expression language, this often means that the outermost syntactic constructor—variable, abstraction, application, conditional, and so on—selects the rule. Syntax-directed rules can frequently be translated directly into recursive type-checking code. Rules such as unrestricted subsumption are not syntax-directed because they can be inserted without regard to the outer form of the expression.^[3]

An algorithmic presentation resolves or controls such choices and specifies how information flows through the rules. It is normally related to the declarative presentation by metatheoretic results:

Soundness: every judgment produced by the algorithmic system is valid in the declarative system.
Completeness: every relevant declaratively valid input is accepted by the algorithmic system, sometimes after explicit type annotations have been inserted.

Termination is additionally required for the rules to constitute a decision procedure.

A classic example is the Hindley–Milner type system. Damas and Milner first give a declarative inference system and then a distinct procedure, Algorithm W, for computing type schemes. They prove that the algorithm is sound and complete with respect to their inference system and that it computes a principal type scheme for every typable expression in the language considered.^[4]

Bidirectional typing

Bidirectional typing divides the ordinary typing relation into two judgment forms:

\Gamma \vdash e\Rightarrow \tau

means that the type of $e$ is synthesized from $e$ and the context, while

\Gamma \vdash e\Leftarrow \tau

means that $e$ is checked against the already known type $\tau$ . The arrows indicate the direction in which type information flows; other arrow and colon notations are also used.^[3]

For example, variables naturally synthesize their types from the context:

{\frac {x{:}\tau \in \Gamma }{\Gamma \vdash x\Rightarrow \tau }}.

An application can synthesize its result type by first synthesizing a function type and then checking the argument against the function's domain:

{\frac {\Gamma \vdash e_{1}\Rightarrow \tau _{1}\mathbin {\to } \tau _{2}\qquad \Gamma \vdash e_{2}\Leftarrow \tau _{1}}{\Gamma \vdash e_{1}\,e_{2}\Rightarrow \tau _{2}}}.

Conversely, an unannotated abstraction can be checked when an expected function type is available:

{\frac {\Gamma ,x{:}\tau _{1}\vdash e\Leftarrow \tau _{2}}{\Gamma \vdash \lambda x.\,e\Leftarrow \tau _{1}\mathbin {\to } \tau _{2}}}.

A type ascription permits a checked expression to synthesize a type:

{\frac {\Gamma \vdash e\Leftarrow \tau }{\Gamma \vdash (e:\tau )\Rightarrow \tau }}.

Finally, a synthesized type can normally be used in checking mode when it is equal to the expected type:

{\frac {\Gamma \vdash e\Rightarrow \tau \qquad \tau \equiv \sigma }{\Gamma \vdash e\Leftarrow \sigma }}.

In systems with subtyping, the equality condition may instead permit a synthesized subtype to be checked against an expected supertype. In systems with nontrivial definitional equality, the condition invokes the system's conversion procedure.

Bidirectional organization reduces the number of types that rules must guess and identifies where annotations are needed. Completeness is therefore often stated as an annotatability result: a declaratively typable expression can be made bidirectionally typable by adding suitable annotations without changing its computational behavior.^[3] An influential application of these ideas to partial, local inference was developed by Pierce and Turner.^[5]

Role in metatheory

Because a typing relation is inductively generated, a derivation can be analyzed according to its final rule or used as the subject of an inductive proof. This supports inversion arguments, which recover information about an expression and its subexpressions from the last possible typing rule. In ordinary structural systems, important supporting results commonly include weakening, exchange, and substitution lemmas; their precise statements depend on the structure of the contexts.

Typing rules are also related to a language's operational semantics in proofs of type safety. A common formulation consists of:

Preservation or subject reduction: if $\Gamma \vdash e:\tau$ and $e$ takes an evaluation step to $e'$ , then $\Gamma \vdash e':\tau$ .
Progress: a well-typed closed expression is either a value or can take an evaluation step.

Together, these results rule out specified forms of stuck execution for well-typed programs. Other formulations of type safety use evaluation, logical relations, or semantic models rather than exactly this progress-and-preservation decomposition. Typing rules alone do not establish safety; the proof must relate the static rules to the language's dynamic semantics.^[1]^: 51–55^[6]

References

1 2 3 4 5 Harper, Robert (2016). Practical Foundations for Programming Languages (PDF) (2nd ed.). Cambridge: Cambridge University Press. ISBN 978-1-107-15030-0. Retrieved 3 September 2026.
1 2 Pierce, Benjamin C. (2002). Types and Programming Languages. Cambridge, Massachusetts: MIT Press. ISBN 978-0-262-16209-8.
1 2 3 4 Dunfield, Jana; Krishnaswami, Neel (2021). "Bidirectional Typing". ACM Computing Surveys. 54 (5). Article 98. arXiv:1908.05839. doi:10.1145/3450952.
1 2 Damas, Luis; Milner, Robin (1982). "Principal Type-Schemes for Functional Programs". Proceedings of the 9th ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages. POPL '82. Association for Computing Machinery. pp. 207–212. doi:10.1145/582153.582176. ISBN 0-89791-065-6.
↑ Pierce, Benjamin C.; Turner, David N. (January 2000). "Local Type Inference" (PDF). ACM Transactions on Programming Languages and Systems. 22 (1): 1–44. doi:10.1145/345099.345100. Retrieved 3 September 2026.
↑ Wright, Andrew K.; Felleisen, Matthias (1994). "A Syntactic Approach to Type Soundness". Information and Computation. 115 (1): 38–94. doi:10.1006/inco.1994.1093.